diff options
| author | David Aspinall | 1998-10-27 12:14:57 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-27 12:14:57 +0000 |
| commit | 2c397c7f9b03f73a550456b8404b835486b3cff3 (patch) | |
| tree | 83074a5b2f8e81ef4d52957aaf045ca9aef8eb4c /generic/proof-script.el | |
| parent | 9a82ef99c0a9dac2aa988dbce358c10caef2d684 (diff) | |
Renamed proof-invisible-command proof-shell-invisible-command.
Removed superfluous optional 'relaxed' argument from:
proof-shell-invisibile-command,
proof-grab-lock,
proof-start-queue.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 51dd695e..06aa9b6b 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1088,11 +1088,15 @@ Only for use by consenting adults." "History of proof commands read from the minibuffer") (defun proof-execute-minibuffer-cmd () + "Prompt for a command in the minibuffer and send it to proof assistant." (interactive) (let (cmd) - (proof-shell-ready-prover) ;; was (proof-check-process-available 'relaxed) + ;; FIXME note: removed ready-prover call since it's done by + ;; proof-shell-invisible-command anyway. + ;; (proof-shell-ready-prover) + ;; was (proof-check-process-available 'relaxed) (setq cmd (read-string "Command: " nil 'proof-minibuffer-history)) - (proof-invisible-command cmd 'relaxed))) + (proof-shell-invisible-command cmd))) @@ -1145,17 +1149,17 @@ Based on position of point." (defun proof-ctxt () "List context." (interactive) - (proof-invisible-command (concat proof-ctxt-string proof-terminal-string))) + (proof-shell-invisible-command (concat proof-ctxt-string proof-terminal-string))) (defun proof-help () "Print help message giving syntax." (interactive) - (proof-invisible-command (concat proof-help-string proof-terminal-string))) + (proof-shell-invisible-command (concat proof-help-string proof-terminal-string))) (defun proof-prf () "List proof state." (interactive) - (proof-invisible-command (concat proof-prf-string proof-terminal-string))) + (proof-shell-invisible-command (concat proof-prf-string proof-terminal-string))) |