[nongnu] elpa/idris-mode d6f54bb121 11/12: Merge pull request #594 from keram/list-holes-no-process-main

[ELPA Syncer]

branch: elpa/idris-mode
commit d6f54bb121599ace73991a4426cf0043decceb93
Merge: 3506c39f5e fd0d7b7918
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #594 from keram/list-holes-no-process-main
    
    Make sure the current file is loaded when listing holes
---
 idris-commands.el |  4 +++-
 idris-tests.el    | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/idris-commands.el b/idris-commands.el
index 9641255854..ec2d6c8312 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -923,8 +923,10 @@ type-correct, so loading will fail."
                 :exclusive 'no))))))
 
 (defun idris-list-holes ()
-  "Get a list of currently-open holes"
+  "Get a list of currently open holes."
   (interactive)
+  (when (idris-current-buffer-dirty-p)
+    (save-excursion (idris-load-file-sync)))
   (idris-hole-list-show (car (idris-eval '(:metavariables 80)))))
 
 (defun idris-list-compiler-notes ()
diff --git a/idris-tests.el b/idris-tests.el
index 1020030b3a..eaf489ebd9 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -107,6 +107,25 @@ remain."
   ;; More cleanup
   (idris-quit))
 
+(ert-deftest idris-list-holes ()
+  "Test `idris-list-holes' command."
+  (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
+        (other-buffer (find-file-noselect "test-data/MakeWithBlock.idr")))
+    ;; Test that hole info is present without need to load file manually
+    (with-current-buffer buffer
+      (idris-list-holes)
+      (dotimes (_ 5) (accept-process-output nil 1))
+      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+        (should (bufferp holes-buffer))
+        (should (> (buffer-size holes-buffer) 10))))
+    ;; Test that the hole info is updated for the other current buffer
+    (with-current-buffer other-buffer
+      (idris-list-holes)
+      (dotimes (_ 5) (accept-process-output nil 1))
+      (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+        (should (not (bufferp holes-buffer)))))
+    (idris-quit)))
+
 (ert-deftest idris-test-proof-search ()
   "Test that proof search works"
   :expected-result (if (string-match-p "idris2" idris-interpreter-path)