diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-shell.el | 10 | ||||
| -rw-r--r-- | plastic/plastic.el | 2 |
4 files changed, 10 insertions, 10 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 778e104f..eff09dd7 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3499,7 +3499,7 @@ a symbol, set to the callback command which is executed in the proof shell filter once @samp{string} has been processed. The @samp{action} variable suggests what class of command is about to be inserted: @lisp - @code{'proof-shell-done-invisible} A non-scripting command + @code{'proof-done-invisible} A non-scripting command @code{'proof-done-advancing} A "forward" scripting command @code{'proof-done-retracting} A "backward" scripting command @end lisp diff --git a/generic/proof-config.el b/generic/proof-config.el index e5bf8e52..36bac31f 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1408,9 +1408,9 @@ a symbol, set to the callback command which is executed in the proof shell filter once `string' has been processed. The `action' variable suggests what class of command is about to be inserted: - 'proof-shell-done-invisible A non-scripting command - 'proof-done-advancing A \"forward\" scripting command - 'proof-done-retracting A \"backward\" scripting command + 'proof-done-invisible A non-scripting command + 'proof-done-advancing A \"forward\" scripting command + 'proof-done-retracting A \"backward\" scripting command Caveats: You should be very careful about setting this hook. Proof General relies on a careful synchronization with the process between diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c53a4d0f..9b2ecf0b 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1648,13 +1648,13 @@ in some cases. May be called by proof-shell-invisible-command." (sit-for 0))) -(defun proof-shell-done-invisible (span) +(defun proof-done-invisible (span) "Callback for proof-shell-invisible-command. Calls proof-state-change-hook." (run-hooks 'proof-state-change-hook)) ; new code to go in after 3.0 -;(defun proof-shell-done-invisible (&optional span) +;(defun proof-done-invisible (&optional span) ; "Callback for proof-shell-invisible-command. ;Calls proof-state-change-hook." ; (run-hooks 'proof-state-change-hook) @@ -1669,14 +1669,14 @@ Calls proof-state-change-hook." ; "Construct a value for `proof-shell-handle-error-or-interrupt-hook'. ;Give error message ERRORMSG, then remove self from queue." ; `(lambda () -; (proof-shell-done-invisible) +; (proof-done-invisible) ; (error ,(eval errormsg)))) ;(defmacro proof-shell-invisible-failure-fn (fn) ; "Construct a value for `proof-shell-handle-error-or-interrupt-hook'. ;Call function fn, then remove self from queue." ; `(lambda () -; (proof-shell-done-invisible) +; (proof-done-invisible) ; (,(eval fn)))) ; ; extra arg ERRORMSGFN to proof-shell-invisible-command: @@ -1701,7 +1701,7 @@ If WAIT is an integer, wait for that many seconds afterwards." (if (not (string-match proof-re-end-of-cmd cmd)) (setq cmd (concat cmd proof-terminal-string))) (proof-start-queue nil nil - (list (list nil cmd 'proof-shell-done-invisible))) + (list (list nil cmd 'proof-done-invisible))) (if wait (proof-shell-wait (if (numberp wait) wait)))) diff --git a/plastic/plastic.el b/plastic/plastic.el index 30561b16..f9ee3df8 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -654,7 +654,7 @@ We assume that module identifiers coincide with file names." ;; Interface to proof-shell-insert now requires two args (for the ;; sake of plastic!) and shouldn't be called from PG instances (proof-shell-insert (concat plastic-lit-string " &S Undo;") - 'proof-shell-done-invisible)) + 'proof-done-invisible)) (defun plastic-try-cmd () "undo whatever was tried, if error-free" |