From 446c67cec7b45d161925fae4b7ef4c045a2336b6 Mon Sep 17 00:00:00 2001
From: Marek L <nospam.keram@gmail.com>
Date: Mon, 19 Dec 2022 18:56:09 +0100
Subject: [PATCH] Ensure Idris connection when running interactive cmd
 `idris-thing-at-point`

Why:
To improve user experience by avoiding unnecessary error.
"Buffer X has no process"
---
 idris-commands.el |  2 ++
 idris-tests.el    | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/idris-commands.el b/idris-commands.el
index 5f4faf20..1d489758 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -338,6 +338,8 @@ compiler-annotated output. 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 eaf489eb..018a7586 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -261,6 +261,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