[ fix ] compile-and-execute menu

idris2-commands.el

@@ -771,11 +771,11 @@ KILLFLAG is set if N was explicitly specified."
                 "idris2-make-lemma: recieved an unsupported \
 'provisional-definition-lemma' response. Ignored.")))))))
 
-(defun idris2-compile-and-execute ()
+(defun idris2-compile-and-execute (name)
   "Execute the program in the current buffer"
-  (interactive)
+  (interactive "MExpression to compile & execute: ")
   (idris2-load-file-sync)
-  (idris2-eval '(:interpret ":exec")))
+  (idris2-repl-eval-string (format ":exec %s" name) 0))
 
 (defun idris2-proof-search (&optional _arg)
   "Invoke the proof search. A plain prefix argument causes the

idris2-mode.el

@@ -70,7 +70,6 @@
     ["Load file" idris2-load-file t]
     ["Choose packages" idris2-set-idris2-load-packages t]
     ["Compile and execute" idris2-compile-and-execute]
-    ["Delete IBC file" idris2-delete-ibc t]
     ["View compiler log" idris2-view-compiler-log (get-buffer idris2-log-buffer-name)]
     ["Quit inferior idris2 process" idris2-quit t]
     "-----------------"

idris2-repl.el

@@ -412,7 +412,7 @@ Invokes `idris2-repl-mode-hook'."
 
 
 (defun idris2-repl-insert-result (string &optional highlighting)
-  "Insert STRING and mark it asg evaluation result.
+  "Insert STRING and mark it as evaluation result.
 Optional argument HIGHLIGHTING is a collection of semantic
 highlighting information from Idris2."
   (with-current-buffer (idris2-repl-buffer)