branch: elpa/idris-mode
commit a47903d2e12532ede66e7cd939e03d0fa2a1b549
Merge: c7c5abaea7 bf262eb187
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #599 from keram/idris-type-at-point-with-process
Ensure Idris connection exist when running `idris-thing-at-point`
---
idris-commands.el | 2 ++
idris-tests.el | 28 ++++++++++++++++++++++++++++
2 files changed, 30 insertions(+)
diff --git a/idris-commands.el b/idris-commands.el
index befa67b5f3..b88980042f 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -338,6 +338,8 @@ Does not return a line number."
(interactive "P")
(let ((name (if thing (read-string "Check: ")
(idris-name-at-point))))
+ (when (idris-current-buffer-dirty-p)
+ (idris-load-file-sync))
(when name
(idris-info-for-name :type-of name))))
diff --git a/idris-tests.el b/idris-tests.el
index eaf489ebd9..47798b24cb 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -124,6 +124,9 @@ remain."
(dotimes (_ 5) (accept-process-output nil 1))
(let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
(should (not (bufferp holes-buffer)))))
+
+ (kill-buffer buffer)
+ (kill-buffer other-buffer)
(idris-quit)))
(ert-deftest idris-test-proof-search ()
@@ -261,6 +264,31 @@ myReverse xs = revAcc [] xs where
(kill-buffer)
(idris-quit)))
+(ert-deftest idris-test-idris-type-at-point ()
+ "Test that `idris-type-at-point' works."
+ (let ((buffer (find-file-noselect "test-data/AddClause.idr")))
+ ;; Assert that we have clean global test state
+ (should (not idris-connection))
+ (with-current-buffer buffer
+ (goto-char (point-min))
+ (re-search-forward "data Test")
+ (funcall-interactively 'idris-type-at-point nil)
+ ;; Assert that Idris connection is created
+ (should idris-connection)
+ ;; Assert that focus is in the Idris info buffer
+ (should (string= (buffer-name) idris-info-buffer-name))
+ ;; Assert that the info buffer displays a type
+ (should (string-match-p "Test : Type" (buffer-substring-no-properties
(point-min) (point-max))))
+
+ ;; TODO: How to emulate "q" key binding to quit info buffer?
+ (idris-info-quit)
+ ;; Assert leaving info buffer will get us back to Idris code buffer
+ (should (eq (current-buffer) buffer))
+
+ ;; Cleanup
+ (kill-buffer))
+ (idris-quit)))
+
(ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
"Test idris-backard-toplevel navigation command."
(idris-test-with-temp-buffer
