branch: elpa/idris-mode
commit 6afe9a82b8011e093491d979dbf02864e357b587
Merge: b7c50dd60f cb71c82e13
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@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
