emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/idris-mode e350ed25a5 3/5: Update `idris-compile-and-execu


From: ELPA Syncer
Subject: [nongnu] elpa/idris-mode e350ed25a5 3/5: Update `idris-compile-and-execute` for Idris2
Date: Tue, 29 Nov 2022 11:59:07 -0500 (EST)

branch: elpa/idris-mode
commit e350ed25a5bf711673412acde6fe945346423a56
Author: Marek L <nospam.keram@gmail.com>
Commit: Marek L <nospam.keram@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.allais@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.")



reply via email to

[Prev in Thread] Current Thread [Next in Thread]