updated;

1 files changed, 65 insertions, 16 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e16e546d..9d350f84 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2633,11 +2633,14 @@ You must set this variable.
 @defvar proof-comment-start 
 String which starts a comment in the proof assistant command language.@*
 The script buffer's @code{comment-start} is set to this string plus a space.
+Moreover, comments are ignored during script management, and not
+sent to the proof process.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-comment-end
 @defvar proof-comment-end 
 String which ends a comment in the proof assistant command language.@*
 The script buffer's @code{comment-end} is set to this string plus a space.
+See also @samp{@code{proof-comment-start}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-case-fold-search
 @defvar proof-case-fold-search 
@@ -2710,20 +2713,30 @@ work for goal..saves is calculated from @code{proof-goal-with-hole-regexp},
 @c TEXI DOCSTRING MAGIC: nilproof-goal-command-p nil 
 @c TEXI DOCSTRING MAGIC: proof-lift-global
 @defvar proof-lift-global 
-This function lifts local lemmas from inside goals out to top level.@*
-This function takes the local goalsave span as an argument. Set this
-to @samp{nil} if the proof assistant does not support nested goals.
+Function which lifts local lemmas from inside goals out to top level.@*
+This function takes the local goalsave span as an argument. Leave this
+set this at @samp{nil} if the proof assistant does not support nested goals,
+or if you don't want to write a function to do move them around.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-count-undos-fn
 @defvar proof-count-undos-fn 
-Compute number of undos in a target segment
+Function to compute number of undos in a target segment.@*
+This is an important function for script management.
+Study one of the existing instantiations for examples of how to write it.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn
 @defvar proof-find-and-forget-fn 
 Function that returns a command to forget back to before its argument span.@*
 This setting is used to for retraction (undoing) in proof scripts.
 
+It should undo the effect of all settings between its target span
+up to (proof-unlocked-begin).  This may involve forgetting a number
+of definitions, declarations, or whatever.
+
 The special string @code{proof-no-command} means there is nothing to do.
+
+This is an important function for script management.
+Study one of the existing instantiations for examples of how to write it.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn
 @defvar proof-goal-hyp-fn 
@@ -2754,7 +2767,9 @@ Hook run when a buffer is switched into scripting mode.@*
 The current buffer will be the newly active scripting buffer.
 
 This hook may be useful for synchronizing with the proof
-assistant, for example, to switch to a new theory.
+assistant, for example, to switch to a new theory
+(in case that isn't already done by commands in the proof
+script).
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-stack-to-indent
 @defvar proof-stack-to-indent 
@@ -2804,7 +2819,7 @@ Emacs.
 
 @c TEXI DOCSTRING MAGIC: proof-prog-name
 @defvar proof-prog-name 
-System command to run program name in proof shell.@*
+System command to run the proof assistant in the proof shell.@*
 Suggestion: this can be set in @code{proof-pre-shell-start-hook} from
 a variable which is in the proof assistant's customization
 group.  This allows different proof assistants to coexist
@@ -2819,7 +2834,7 @@ print a welcome message.
 Note that it is sent before Proof General's synchronization
 mechanism is engaged (in case the command engages it).  It
 is better to configure the proof assistant via command
-line options is possible.
+line options if possible.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
 @defvar proof-shell-restart-cmd 
@@ -2844,7 +2859,7 @@ directory the file resides in.
 
 NB: By default, @code{proof-cd} is called from @code{proof-activate-scripting-hook},
 so that the prover switches to the directory of a proof
-script everytime scripting begins.
+script every time scripting begins.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd
 @defvar proof-shell-inform-file-processed-cmd 
@@ -2862,9 +2877,30 @@ issuing this command.
 
 If this is set to nil, no command is issued.
 
-See also @code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
+See also: @code{proof-shell-inform-file-retracted-cmd}, 
+@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd
+@defvar proof-shell-inform-file-retracted-cmd 
+Command to the proof assistant to tell it that a file has been retracted.@*
+The format character %s is replaced by a complete filename for a
+script file which Proof General wants the prover to consider
+as not completely processed.
+
+This is used to interface with the proof assistant's internal
+management of multiple files, so the proof assistant is kept aware of
+which files have been processed.  Specifically, when scripting
+is activated, the file is removed from Proof General's list of 
+processed files, and the prover is told about it by issuing this 
+command.  The action may cause the prover in turn to suggest to 
+Proof General that files depending on this one are
+also unlocked.
+
+If this is set to nil, no command is issued.
+
+See also: @code{proof-shell-inform-file-processed-cmd}, 
+@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
+@end defvar
 
 
 @node Settings for matching output from proof process
@@ -2882,7 +2918,7 @@ and are stripped from the prover's output strings.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern
 @defvar proof-shell-prompt-pattern 
-Proof shell's value for comint-prompt-pattern.
+Proof shell's value for comint-prompt-pattern, which see.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp
 @defvar proof-shell-annotated-prompt-regexp 
@@ -2917,9 +2953,9 @@ It is safe to leave this variable unset (as nil).
 @c TEXI DOCSTRING MAGIC: proof-shell-interrupt-regexp
 @defvar proof-shell-interrupt-regexp 
 Regexp matching output indicating the assistant was interrupted.@*
-We assume that an error message corresponds to a failure in the last
+We assume that an interrupt message corresponds to a failure in the last
 proof command executed.  So don't match mere warning messages with
-this regexp.  Moreover, an error message should not be matched as an
+this regexp.  Moreover, an interrupt message should not be matched as an
 eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it
 will be lost.
 
@@ -2931,6 +2967,10 @@ It is safe to leave this variable unset (as nil).
 @defvar proof-shell-proof-completed-regexp 
 Regexp matching output indicating a finished proof.@*
 Match number 1 should be the response text.
+
+This is used to enable the QED function (save a proof) and
+to control what output appears in the response buffer at the
+end of a proof.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-clear-response-regexp
 @defvar proof-shell-clear-response-regexp 
@@ -2940,7 +2980,10 @@ is shown to the user.  Set to nil to disable.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp
 @defvar proof-shell-start-goals-regexp 
-Regexp matching the start of the proof state output.
+Regexp matching the start of the proof state output.@*
+This is an important setting.  Output between @samp{@code{proof-shell-start-goals-regexp}}
+and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
+and possibly analysed further for proof-by-pointing markup.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
 @defvar proof-shell-end-goals-regexp 
@@ -2989,7 +3032,7 @@ NB: You should be very careful about setting this hook.  Proof General
 relies on a careful synchronization with the process between inputs
 and outputs.  It expects to see a prompt for each input it sends from
 the queue.  If you add extra input here and it causes more prompts
-than expected, things will break!  Massaging the @var{string} variable
+than expected, things will break!  Massaging the variable @var{string}
 may be safer since it is stripped of carriage returns 
 before being sent.
 @end defvar
@@ -2997,7 +3040,7 @@ before being sent.
 @c TEXI DOCSTRING MAGIC: proof-pre-shell-start-hook
 @defvar proof-pre-shell-start-hook 
 Hooks run before proof shell is started.@*
-This may be set to a function which configures the proof shell
+Suggestion: set this to a function which configures the proof shell
 variables.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-handle-error-hook
@@ -3462,7 +3505,13 @@ variables @code{proof-included-files-list} documented earlier
 @defun proof-register-possibly-new-processed-file file &optional informprover
 Register a possibly new @var{file} as having been processed by the prover.@*
 If @var{informprover} is non-nil, the proof assistant will be told about this,
-to co-ordinate with its internal file-management.
+to co-ordinate with its internal file-management.  (Otherwise we assume
+that it is a message from the proof assistant which triggers this call).
+
+No action is taken if the file is already registered.
+
+A warning message is issued if the register request came from the
+proof assistant and Emacs is has a modified buffer visiting the file.
 @end defun
 
 Another important function activates scripting for the current script