Skip to content

Ensure Idris is running and current idr file loaded when using idris-switch-to-repl #643

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Ensure Idris is running and current idr file loaded when using idris-switch-to-repl #643

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions idris-common-utils.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -365,15 +365,15 @@ corresponding values in the CDR of VALUE."
'()
`((t (error "ELISP destructure-case failed: %S" ,tmp))))))))

(defun idris-idr-p (&optional buffer)
"Return t if BUFFER is an Idris file (.idr)."
(if-let* ((file-name (buffer-file-name buffer)))
(string-equal (downcase (file-name-extension file-name)) "idr")))

(defun idris-lidr-p (&optional buffer)
"Return t if BUFFER is a literate Idris file, or nil otherwise.
Use the current buffer if BUFFER is not supplied or is nil."
(let ((file-name (buffer-file-name buffer)))
;; We check for nil here because idris-lidr-p might be called on
;; buffers that don't have associated files, such as the REPL
;; buffer or an info buffer
(and (stringp file-name)
(string= (file-name-extension file-name) "lidr"))))
"Return t if BUFFER is a literate Idris file (.lidr)."
(if-let* ((file-name (buffer-file-name buffer)))
(string-equal (downcase (file-name-extension file-name)) "lidr")))

(defun idris-make-file-link-overlay (start end keymap help-echo)
(let ((overlay (make-overlay start end)))
Expand Down
10 changes: 8 additions & 2 deletions idris-repl.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,9 +186,14 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the end of the buffer."
(idris-repl-insert-prompt)
(insert current-input))))

(autoload 'idris-load-file-sync "idris-commands.el")
;;;###autoload
(defun idris-switch-to-repl ()
"Select the output buffer and scroll to bottom."
"Load the current Idris file buffer and jump to the Idris REPL."
(interactive)
(if (or (idris-idr-p) (idris-lidr-p))
(idris-load-file-sync)
Copy link
Contributor Author

@keram keram Sep 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using synchronous load as async idris-load-file causes point to be moved from repl back to source file.

(user-error "This command can only be run from a buffer visiting an Idris `.idr' or `.lidr' file"))
(pop-to-buffer (idris-repl-buffer))
(goto-char (point-max)))

Expand All @@ -199,7 +204,8 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the end of the buffer."
(defun idris-repl ()
(interactive)
(idris-run)
(idris-switch-to-repl))
(pop-to-buffer (idris-repl-buffer))
(goto-char (point-max)))

(defvar idris-repl-mode-map
(let ((map (make-sparse-keymap)))
Expand Down