branch: elpa/idris-mode
commit e350ed25a5bf711673412acde6fe945346423a56
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Update `idris-compile-and-execute` for Idris2
Backport of idris2-compile-and-execute from
https://github.com/idris-community/idris2-mode/pull/20/files
with preserving backward compatibility for Idris 1
Co-authored-by: "G. Allais" <guillaume.all...@ens-lyon.org>
---
idris-commands.el | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index da73e2be89..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.")
