diff options
| author | David Aspinall | 1998-11-25 13:05:36 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-25 13:05:36 +0000 |
| commit | 7af7d1fdae2d78f5e76bf3e82a656d44dc157e9d (patch) | |
| tree | de3f4790372fb1ca0095ff533bfc0dd7f6110c30 /generic/proof-shell.el | |
| parent | 0702539ad300891ca5590aa552d893fe1561505c (diff) | |
Docstring improvements.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 9 |
1 files changed, 6 insertions, 3 deletions
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 |