From 2c397c7f9b03f73a550456b8404b835486b3cff3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 27 Oct 1998 12:14:57 +0000 Subject: Renamed proof-invisible-command proof-shell-invisible-command. Removed superfluous optional 'relaxed' argument from: proof-shell-invisibile-command, proof-grab-lock, proof-start-queue. --- generic/proof-script.el | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'generic/proof-script.el') 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))) -- cgit v1.2.3