diff options
| author | David Aspinall | 1998-11-25 12:31:52 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-25 12:31:52 +0000 |
| commit | d2b9b0555e7cf208e06eb6490dc70cc67daca239 (patch) | |
| tree | 6c4da98b052ace038949ea462312e627118d3226 /generic/proof-script.el | |
| parent | c91765f2c59ff1b8855f18760b124efda2ad7778 (diff) | |
Improved docstrings
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 7f248dba..7a72a142 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -389,8 +389,17 @@ will become the current scripting buffer provided the current scripting buffer has either no locked region or everything in it has been processed. +If we're changing scripting buffer and the old one is associated with +a file, add it to proof-included-files-list. + When a new script buffer has scripting minor mode turned on, -the hooks `proof-activate-scripting-hook' are run." +the hooks `proof-activate-scripting-hook' are run. This can +be a useful place to configure the proof assistant for +scripting in a particular file, for example, loading the +correct theory, or whatever. + +Finally, this may be a good time to ask if the user wants to save some +buffers." (cond ((not (eq proof-buffer-type 'script)) (error "Must be running in a script buffer")) @@ -445,7 +454,6 @@ the hooks `proof-activate-scripting-hook' are run." ;; This may be a good time to ask if the user wants to save some ;; buffers - ;; FIXME: no, move it elsewhere. (save-some-buffers)))) |