branch: elpa/idris-mode
commit fd0d7b7918ddd024552224487929334ce86bd03e
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Make sure the current file is loaded when listing holes
Why:
To improve user experience.
Currently when user try list holes without loading
the file first he gets error: "Buffer X has no process".
Also when user switch to new Idris file and try to list holes,
the holes are displayed for the previous buffer.
This change ensures that the holes info is alway up to date.
---
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 c1c8f3bfcd..90f5b7432d 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -922,8 +922,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 5bc9d5153f..c42c7af5bb 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)
