[nongnu] elpa/idris-mode a47903d2e1 5/5: Merge pull request #599 from keram/idris-type-at-point-with-process

[ELPA Syncer]

branch: elpa/idris-mode
commit a47903d2e12532ede66e7cd939e03d0fa2a1b549
Merge: c7c5abaea7 bf262eb187
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@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