Improved docstrings

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