branch: elpa/idris-mode
commit 306420713dc561f6294354ef6c44c842f0426abb
Merge: 6afe9a82b8 28758e0980
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #603 from keram/impro-code3
Codebase improvements 2
---
idris-commands.el | 42 ------------------------------------------
idris-common-utils.el | 43 +++++++++++++++++++++++++++++++++++++++++++
idris-compat.el | 7 +++++++
idris-repl.el | 5 +++--
idris-tests.el | 40 ++++++++++++++++++++++------------------
5 files changed, 75 insertions(+), 62 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 040ecf75a5..88f5c590ab 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -48,15 +48,6 @@
(defvar-local idris-load-to-here nil
"The maximum position to load.")
-(defun idris-get-line-num (position)
- "Get the absolute line number at POSITION."
- ;; In Emacs 26.1 > line-number-at-pos accepts
- ;; additional optional argument ABSOLUTE which
- ;; removes need for `save-restriction' and `widen'
- (save-restriction
- (widen)
- (line-number-at-pos position)))
-
(defun idris-make-dirty ()
"Mark an Idris buffer as dirty and remove the loaded region."
(setq idris-buffer-dirty-p t)
@@ -291,39 +282,6 @@ This sets the load position to point, if there is one."
(error "Cannot find file for current buffer")))
-(defun idris-operator-at-position-p (pos)
- "Return t if syntax lookup is `.' or char after POS is `-'."
- (or (equal (syntax-after pos) (string-to-syntax "."))
- (eq (char-after pos) ?-)))
-
-(defun idris-thing-at-point ()
- "Return the line number and name at point as a cons.
-Use this in Idris source buffers."
- (let ((line (idris-get-line-num (point))))
- (cons
- (if (idris-operator-at-position-p (point))
- (save-excursion
- (skip-syntax-backward ".")
- (let ((beg (point)))
- (skip-syntax-forward ".")
- (buffer-substring-no-properties beg (point))))
- ;; Try if we're on a symbol or fail otherwise.
- (or (current-word t)
- (error "Nothing identifiable under point")))
- line)))
-
-(defun idris-name-at-point ()
- "Return the name at point, taking into account semantic annotations.
-Use this in Idris source buffers or in compiler-annotated output.
-Does not return a line number."
- (let ((ref (cl-remove-if
- #'null
- (cons (get-text-property (point) 'idris-ref)
- (cl-loop for overlay in (overlays-at (point))
- collecting (overlay-get overlay 'idris-ref))))))
- (if (null ref)
- (car (idris-thing-at-point))
- (car ref))))
(defun idris-info-for-name (what name)
"Display the type for a NAME."
diff --git a/idris-common-utils.el b/idris-common-utils.el
index 935116ad87..3b18bbfc32 100644
--- a/idris-common-utils.el
+++ b/idris-common-utils.el
@@ -416,4 +416,47 @@ relative to SRC-DIR"
(and (>= idris-protocol-version major)
(>= idris-protocol-version-minor minor))))
+(defun idris-get-line-num (position)
+ "Get the absolute line number at POSITION."
+ ;; In Emacs 26.1 > line-number-at-pos accepts
+ ;; additional optional argument ABSOLUTE which
+ ;; removes need for `save-restriction' and `widen'
+ (save-restriction
+ (widen)
+ (line-number-at-pos position)))
+
+(defun idris-operator-at-position-p (pos)
+ "Return t if syntax lookup is `.' or char after POS is `-'."
+ (or (equal (syntax-after pos) (string-to-syntax "."))
+ (eq (char-after pos) ?-)))
+
+(defun idris-thing-at-point ()
+ "Return the line number and name at point as a cons.
+Use this in Idris source buffers."
+ (let ((line (idris-get-line-num (point))))
+ (cons
+ (if (idris-operator-at-position-p (point))
+ (save-excursion
+ (skip-syntax-backward ".")
+ (let ((beg (point)))
+ (skip-syntax-forward ".")
+ (buffer-substring-no-properties beg (point))))
+ ;; Try if we're on a symbol or fail otherwise.
+ (or (current-word t)
+ (user-error "Nothing identifiable under point")))
+ line)))
+
+(defun idris-name-at-point ()
+ "Return the name at point, taking into account semantic annotations.
+Use this in Idris source buffers or in compiler-annotated output.
+Does not return a line number."
+ (let ((ref (cl-remove-if
+ #'null
+ (cons (get-text-property (point) 'idris-ref)
+ (cl-loop for overlay in (overlays-at (point))
+ collecting (overlay-get overlay 'idris-ref))))))
+ (if (null ref)
+ (car (idris-thing-at-point))
+ (car ref))))
+
(provide 'idris-common-utils)
diff --git a/idris-compat.el b/idris-compat.el
index 2811f01bc8..d248d7f872 100644
--- a/idris-compat.el
+++ b/idris-compat.el
@@ -34,5 +34,12 @@ attention to case differences."
(unless (fboundp 'gensym)
(defalias 'gensym 'cl-gensym))
+(if (fboundp 'file-name-concat)
+ (defalias 'idris-file-name-concat 'file-name-concat)
+ (defun idris-file-name-concat (&rest components)
+ (let ((dirs (butlast components)))
+ (concat (apply 'concat (mapcar 'file-name-as-directory dirs))
+ (car (reverse components))))))
+
(provide 'idris-compat)
;;; idris-compat.el ends here
diff --git a/idris-repl.el b/idris-repl.el
index 910f253603..108b02fa0c 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -548,8 +548,9 @@ The handler will use qeuery to ask the use if the error
should be ingored."
Use `idris-repl-history-file' if set or fallback
to filepath computed from the `idris-interpreter-path'."
(or idris-repl-history-file
- ;; We should use `file-name-concat' but it is only in Emacs version 28+
- (concat "~/." (file-name-nondirectory idris-interpreter-path)
"/idris-history.eld")))
+ (idris-file-name-concat "~"
+ (concat "." (file-name-nondirectory
idris-interpreter-path))
+ "idris-history.eld")))
(defun idris-repl-read-history-filename ()
(read-file-name "Use Idris REPL history from file: "
diff --git a/idris-tests.el b/idris-tests.el
index 2d79f4162c..2c3e9f5ac6 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -134,24 +134,25 @@ remain."
:expected-result (if (string-match-p "idris2" idris-interpreter-path)
:failed
:passed)
- (let ((buffer (find-file "test-data/ProofSearch.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 1))
- (goto-char (point-min))
- (re-search-forward "search_here")
- (goto-char (match-beginning 0))
- (idris-proof-search)
- (dotimes (_ 5) (accept-process-output nil 1))
- (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc
lteZero))))"))
- (move-beginning-of-line nil)
- (delete-region (point) (line-end-position))
- (insert "prf = ?search_here")
- (save-buffer)
- (kill-buffer)))
-
- ;; More cleanup
- (idris-quit))
+ (unwind-protect
+ (let ((buffer (find-file "test-data/ProofSearch.idr")))
+ (with-current-buffer buffer
+ (idris-load-file)
+ (dotimes (_ 5) (accept-process-output nil 1))
+ (goto-char (point-min))
+ (re-search-forward "search_here")
+ (goto-char (match-beginning 0))
+ (idris-proof-search)
+ (dotimes (_ 5) (accept-process-output nil 1))
+ (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc
lteZero))))"))
+ (move-beginning-of-line nil)
+ (delete-region (point) (line-end-position))
+ (insert "prf = ?search_here")
+ (save-buffer)
+ (kill-buffer)))
+
+ ;; More cleanup
+ (idris-quit)))
(ert-deftest idris-test-find-cmdline-args ()
"Test that idris-mode calculates command line arguments from .ipkg files."
@@ -270,6 +271,9 @@ myReverse xs = revAcc [] xs where
;; Assert that we have clean global test state
(should (not idris-connection))
(with-current-buffer buffer
+ ;; Hack to reduce random failures
+ ;; TODO: Fix the leak
+ (idris-delete-ibc t)
(goto-char (point-min))
(re-search-forward "data Test")
(funcall-interactively 'idris-type-at-point nil)
