Skip to content

Commit

Permalink
[ fix ] compile-and-execute menu (#20)
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais authored May 26, 2022
1 parent 5c39e7c commit a2976d0
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 5 deletions.
6 changes: 3 additions & 3 deletions idris2-commands.el
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion idris2-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -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]
"-----------------"
Expand Down
2 changes: 1 addition & 1 deletion idris2-repl.el
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit a2976d0

Please sign in to comment.