[nongnu] elpa/idris-mode 306420713d 12/13: Merge pull request #603 from keram/impro-code3

[ELPA Syncer]

branch: elpa/idris-mode
commit 306420713dc561f6294354ef6c44c842f0426abb
Merge: 6afe9a82b8 28758e0980
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@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)