diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 12 | ||||
| -rw-r--r-- | generic/proof-shell.el | 2 |
2 files changed, 11 insertions, 3 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)))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 996ffa65..ede3f76d 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -699,7 +699,7 @@ by setting proof-shell-delayed-output to a cons cell of (insert . txt) where TXT is the text to be inserted. To extend this function, set -`proof-shell-process-output-system-specific'. +proof-shell-process-output-system-specific. This function - it can return one of 4 things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this was output from pbp, and |