branch: elpa/idris-mode
commit fdbd019cb284455f0e2e887a833f64c67b89c80f
Merge: a05c2c5fc9 e350ed25a5
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #573 from keram/backport-idris2-compile-and-execute
Update idris-compile-and-execute for Idris2
---
idris-commands.el | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 256458d274..893abb8a98 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -748,12 +748,15 @@ Otherwise, case split as a pattern variable."
;; make sure point is at new defn
(goto-char end)))))))))))
-
(defun idris-compile-and-execute ()
- "Execute the program in the current buffer"
+ "Execute the program in the current buffer."
(interactive)
(idris-load-file-sync)
- (idris-eval '(:interpret ":exec")))
+ (if (>=-protocol-version 2 1)
+ (let ((name (read-string "MExpression to compile & execute (default
main): "
+ nil nil "main")))
+ (idris-repl-eval-string (format ":exec %s" name) 0))
+ (idris-eval '(:interpret ":exec"))))
(defvar-local proof-region-start nil
"The start position of the last proof region.")
@@ -989,7 +992,9 @@ https://github.com/clojure-emacs/cider";
(delete-overlay idris-loaded-region-overlay)
(setq idris-loaded-region-overlay nil)))
(idris-prover-end)
- (idris-kill-buffers)))
+ (idris-kill-buffers)
+ (setq idris-protocol-version 0
+ idris-protocol-version-minor 0)))
(defun idris-delete-ibc (no-confirmation)
"Delete the IBC file for the current buffer. A prefix argument
