[nongnu] elpa/idris-mode 6afe9a82b8 11/13: Merge pull request #602 from keram/impro-code

[ELPA Syncer]

branch: elpa/idris-mode
commit 6afe9a82b8011e093491d979dbf02864e357b587
Merge: b7c50dd60f cb71c82e13
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #602 from keram/impro-code
    
    Codebase improvements
---
 idris-commands.el         | 47 +++++++++++++++++++++++++++++++++++++----------
 idris-common-utils.el     |  2 +-
 idris-keys.el             |  2 +-
 idris-repl.el             |  9 ++++++---
 inferior-idris.el         | 41 ++++-------------------------------------
 test-data/GenerateDef.idr |  2 +-
 6 files changed, 50 insertions(+), 53 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index b88980042f..040ecf75a5 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -939,20 +939,13 @@ type-correct, so loading will fail."
   "Remove Idris event hooks set after connection with Idris established."
   (dolist (h idris-event-hooks) (remove-hook 'idris-event-hooks h)))
 
-(defun idris-pop-to-repl ()
-  "Go to the REPL, if one is open."
-  (interactive)
-  (let ((buf (get-buffer idris-repl-buffer-name)))
-    (if buf
-        (pop-to-buffer buf)
-      (error "No Idris REPL buffer is open"))))
+(define-obsolete-function-alias 'idris-pop-to-repl 'idris-switch-to-repl 
"2022-12-28")
 
 (defun idris-switch-to-last-idris-buffer ()
   "Switch to the last Idris buffer.
 The default keybinding for this command is
-the same as variable `idris-pop-to-repl',
-so that it is very convenient to jump between a
-Idris buffer and the REPL buffer.
+the same as for command `idris-switch-to-repl',
+so it is convenient to jump between Idris code and REPL.
 
 Inspired by `cider-switch-to-last-clojure-buffer'
 https://github.com/clojure-emacs/cider";
@@ -966,6 +959,40 @@ https://github.com/clojure-emacs/cider";
           (user-error "No Idris buffer found")))
     (user-error "Not in a Idris REPL buffer")))
 
+(defun idris-run ()
+  "Run an inferior Idris process."
+  (interactive)
+  (let ((command-line-flags (idris-compute-flags)))
+    ;; Kill the running Idris if the command-line flags need updating
+    (when (and (get-buffer-process (get-buffer idris-connection-buffer-name))
+               (not (equal command-line-flags idris-current-flags)))
+      (message "Idris command line arguments changed, restarting Idris")
+      (idris-quit)
+      (sit-for 0.01)) ; allows the sentinel to run and reset idris-process
+    ;; Start Idris if necessary
+    (when (not idris-process)
+      (setq idris-process
+            (get-buffer-process
+             (apply #'make-comint-in-buffer
+                    "idris"
+                    idris-process-buffer-name
+                    idris-interpreter-path
+                    nil
+                    "--ide-mode-socket"
+                    command-line-flags)))
+      (with-current-buffer idris-process-buffer-name
+        (add-hook 'comint-preoutput-filter-functions
+                  'idris-process-filter
+                  nil
+                  t)
+        (add-hook 'comint-output-filter-functions
+                  'idris-show-process-buffer
+                  nil
+                  t))
+      (set-process-sentinel idris-process 'idris-sentinel)
+      (setq idris-current-flags command-line-flags)
+      (accept-process-output idris-process 3))))
+
 (defun idris-quit ()
   "Quit the Idris process, cleaning up the state synchronized with Emacs."
   (interactive)
diff --git a/idris-common-utils.el b/idris-common-utils.el
index 0af862df57..935116ad87 100644
--- a/idris-common-utils.el
+++ b/idris-common-utils.el
@@ -77,7 +77,7 @@ Lisp package.")
     (when (and buf (buffer-live-p buf))
       (let ((win (get-buffer-window buf)))
         (kill-buffer buf)
-        (when (null (window-prev-buffers win))
+        (when (and (null (window-prev-buffers win)) (< 1 (length 
(window-list))))
           (delete-window win))))
     (when return-buffer (pop-to-buffer return-buffer 
`(display-buffer-reuse-window)))))
 
diff --git a/idris-keys.el b/idris-keys.el
index 7dc5b97027..e639373382 100644
--- a/idris-keys.el
+++ b/idris-keys.el
@@ -75,7 +75,7 @@
 
 (defun idris-define-general-keys (map)
   "Define keys that are generally useful for all Idris modes in the keymap 
MAP."
-  (define-key map (kbd "C-c C-z") 'idris-pop-to-repl)
+  (define-key map (kbd "C-c C-z") 'idris-switch-to-repl)
   (define-key map (kbd "<mouse-3>") 'prop-menu-show-menu)
   (define-key map (kbd "C-c C-SPC") 'prop-menu-by-completing-read))
 
diff --git a/idris-repl.el b/idris-repl.el
index 2baba65ccd..910f253603 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -159,17 +159,20 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at 
the end of the buffer."
       (idris-repl-insert-prompt)
       (insert current-input))))
 
-(defun idris-switch-to-output-buffer ()
+(defun idris-switch-to-repl ()
   "Select the output buffer and scroll to bottom."
   (interactive)
   (pop-to-buffer (idris-repl-buffer))
   (goto-char (point-max)))
 
+(define-obsolete-function-alias 'idris-switch-to-output-buffer 
'idris-switch-to-repl "2022-12-28")
+
+(autoload 'idris-run "idris-commands.el")
 ;;;###autoload
 (defun idris-repl ()
   (interactive)
   (idris-run)
-  (idris-switch-to-output-buffer))
+  (idris-switch-to-repl))
 
 (defvar idris-repl-mode-map
   (let ((map (make-sparse-keymap)))
@@ -189,7 +192,7 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the 
end of the buffer."
                   idris-define-general-keys
                   idris-define-active-term-keys)
              do (funcall keyer map))
-    (substitute-key-definition 'idris-pop-to-repl
+    (substitute-key-definition 'idris-switch-to-repl
                                'idris-switch-to-last-idris-buffer
                                map)
     map)
diff --git a/inferior-idris.el b/inferior-idris.el
index 17fd79574c..a300c72722 100644
--- a/inferior-idris.el
+++ b/inferior-idris.el
@@ -97,42 +97,6 @@ Set using file or directory variables.")
   "The list of `command-line-args' actually passed to Idris.
 This is maintained to restart Idris when the arguments change.")
 
-(autoload 'idris-prover-event-hook-function "idris-prover.el")
-(autoload 'idris-quit "idris-commands.el")
-(defun idris-run ()
-  "Run an inferior Idris process."
-  (interactive)
-  (let ((command-line-flags (idris-compute-flags)))
-    ;; Kill the running Idris if the command-line flags need updating
-    (when (and (get-buffer-process (get-buffer idris-connection-buffer-name))
-               (not (equal command-line-flags idris-current-flags)))
-      (message "Idris command line arguments changed, restarting Idris")
-      (idris-quit)
-      (sit-for 0.01)) ; allows the sentinel to run and reset idris-process
-    ;; Start Idris if necessary
-    (when (not idris-process)
-      (setq idris-process
-            (get-buffer-process
-             (apply #'make-comint-in-buffer
-                    "idris"
-                    idris-process-buffer-name
-                    idris-interpreter-path
-                    nil
-                    "--ide-mode-socket"
-                    command-line-flags)))
-      (with-current-buffer idris-process-buffer-name
-        (add-hook 'comint-preoutput-filter-functions
-                  'idris-process-filter
-                  nil
-                  t)
-        (add-hook 'comint-output-filter-functions
-                  'idris-show-process-buffer
-                  nil
-                  t))
-      (set-process-sentinel idris-process 'idris-sentinel)
-      (setq idris-current-flags command-line-flags)
-      (accept-process-output idris-process 3))))
-
 (defun idris-connect (port)
   "Establish a connection with a Idris REPL at PORT."
   (when (not idris-connection)
@@ -143,7 +107,10 @@ This is maintained to restart Idris when the arguments 
change.")
     (add-hook 'idris-event-hooks 'idris-warning-event-hook-function)
     (add-hook 'idris-event-hooks 'idris-prover-event-hook-function)
 
-    (unless idris-hole-show-on-load
+    (if idris-hole-show-on-load
+        (progn
+          (add-hook 'idris-load-file-success-hook 'idris-list-holes)
+          (add-hook 'idris-prover-success-hook 'idris-list-holes))
       (remove-hook 'idris-load-file-success-hook 'idris-list-holes-on-load)
       (remove-hook 'idris-load-file-success-hook 'idris-list-holes)
       ;; TODO: In future decouple prover sucess hook from being affected by
diff --git a/test-data/GenerateDef.idr b/test-data/GenerateDef.idr
index 885ac9514a..0456cafb86 100644
--- a/test-data/GenerateDef.idr
+++ b/test-data/GenerateDef.idr
@@ -20,7 +20,7 @@ C-c C-r               idris-refine
 C-c C-s                idris-add-clause
 C-c C-t                idris-type-at-point
 C-c C-w                idris-make-with-block
-C-c C-z                idris-pop-to-repl
+C-c C-z                idris-switch-to-repl
 C-c C-S-a      idris-proof-search-next
 C-c C-S-g      idris-generate-def-next
 C-c C-SPC      prop-menu-by-completing-read