branch: elpa/idris-mode
commit d9576861a88aef6e7a40b7bf9f000930b5c07641
Author: Marek L <[email protected]>
Commit: Marek L <[email protected]>
Suppress Idris errors when loading a file in `idris-switch-to-repl`
This improves the user workflow.
When writing Idris code, it is often useful to switch back and forth
to the REPL (e.g., to test functions, look up docs, or check types),
even when the code is in a broken state.
However, when an error occurs, switching to the REPL is interrupted,
leaving the point in the original buffer and forcing the user
to dismiss the Idris notes.
---
idris-repl.el | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/idris-repl.el b/idris-repl.el
index a60e442aa7..32e21801a8 100644
--- a/idris-repl.el
+++ b/idris-repl.el
@@ -191,7 +191,7 @@ If ALWAYS-INSERT is non-nil, always insert a prompt at the
end of the buffer."
(defun idris-switch-to-repl ()
"Load the current Idris file buffer and jump to the Idris REPL."
(interactive nil idris-mode)
- (idris-load-file-sync)
+ (idris-load-file-sync t)
(pop-to-buffer (idris-repl-buffer))
(goto-char (point-max)))
