diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 14 | ||||
| -rw-r--r-- | generic/proof-shell.el | 9 |
2 files changed, 17 insertions, 6 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 1a96b484..3d07a9ac 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1092,7 +1092,11 @@ command." (defun proof-try-command (&optional unclosed-comment-fun) "Process the command at point, but don't add it to the locked region. -This will only happen if the command satisfies proof-state-preserving-p. + +Supplied to let the user to test the types and values of +expressions. Checks via the function proof-state-preserving-p that the +command won't change the proof state, but this isn't guaranteed to be +foolproof and may cause Proof General to lose sync with the prover. Default action if inside a comment is just to go until the start of the comment. If you want something different, put it inside @@ -1145,7 +1149,7 @@ the proof script." ;; here. (defun proof-interrupt-process () - "Interrupt the proof assistant. WARNING! This may confuse Proof General." + "Interrupt the proof assistant. Warning! This may confuse Proof General." (interactive) (if (not (proof-shell-live-buffer)) (error "Proof Process Not Started!")) @@ -1264,7 +1268,11 @@ 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." + "Prompt for a command in the minibuffer and send it to proof assistant. +The command isn't added to the locked region. + +Warning! No checking whatsoever is done on the command, so this is +even more dangerous than proof-try-command." (interactive) (let (cmd) ;; FIXME note: removed ready-prover call since it's done by diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 78b710da..96111565 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -316,8 +316,9 @@ clears up all the locked regions and state variables." (defun proof-shell-exit () "Query the user and exit the proof process. + This simply kills the proof-shell-buffer relying on the hook function -to do the hard work." +proof-shell-kill-function to do the hard work." (interactive) (if (buffer-live-p proof-shell-buffer) (if (yes-or-no-p (format "Exit %s process? " proof-assistant)) @@ -333,8 +334,10 @@ ensuring that script buffers are cleaned up neatly." (kill-buffer proof-shell-buffer)) (defun proof-shell-restart () - "Restart the proof shell by sending the restart command -and clearing all script buffers." + "Clear script buffers and send proof-shell-restart-cmd. +All locked regions are cleared and the active scripting buffer +deactivated. The restart command should re-synchronize +Proof General with the proof assitant." (interactive) (proof-script-remove-all-spans-and-deactivate) (setq proof-included-files-list nil |