docstring magic

1 files changed, 131 insertions, 46 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 5522f96e..fe890a14 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1027,8 +1027,8 @@ Process the current buffer and set point at the end of the buffer.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-retract-buffer
-@deffn Command proof-process-buffer 
-Process the current buffer and set point at the end of the buffer.
+@deffn Command proof-retract-buffer 
+Retract the current buffer and set point at the start of the buffer.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-active-terminator-minor-mode
@@ -1088,6 +1088,9 @@ Clear script buffers and send @code{proof-shell-restart-cmd}.@*
 All locked regions are cleared and the active scripting buffer
 deactivated.  
 
+If the proof shell is busy, an interrupt is sent with
+@code{proof-interrupt-process} and we wait until the process is ready. 
+
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
 process.  
@@ -1136,20 +1139,20 @@ from a proof script.  Here are the keybindings and functions.
 @c TEXI DOCSTRING MAGIC: proof-prf
 @deffn Command proof-prf 
 Show the current proof state.@*
-Issues a command to the assistant from @code{proof-showproof-command}.
+Issues a command to the assistant based on @code{proof-showproof-command}.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-ctxt
 @deffn Command proof-ctxt 
 Show the current context.@*
-Issues a command to the assistant from @code{proof-context-command}.
+Issues a command to the assistant based on @code{proof-context-command}.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-help
 @deffn Command proof-help 
 Show a help or information message from the proof assistant.@*
 Typically, a list of syntax of commands available.
-Issues a command to the assistant from @code{proof-info-command}.
+Issues a command to the assistant based on @code{proof-info-command}.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-find-theorems
@@ -1169,8 +1172,10 @@ Interrupt the proof assistant.  Warning! This may confuse Proof General.
 Prompt for a command in the minibuffer and send it to proof assistant.@*
 The command isn't added to the locked region.
 
-Warning! No checking whatsoever is done on the command, so this is
-even more dangerous than @code{proof-try-command}.
+If @code{proof-state-preserving-p} is configured, it is used as a check
+that the command will be safe to execute, in other words, that
+it won't ruin synchronization.  If applied to the command it 
+returns false, then an error message is given.
 @end deffn
 
 As if the last two commands weren't risky enough, there's also a command
@@ -1199,6 +1204,9 @@ Clear script buffers and send @code{proof-shell-restart-cmd}.@*
 All locked regions are cleared and the active scripting buffer
 deactivated.  
 
+If the proof shell is busy, an interrupt is sent with
+@code{proof-interrupt-process} and we wait until the process is ready. 
+
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
 process.  
@@ -1648,6 +1656,7 @@ The default value is @code{nil}.
 @cindex Remote host
 @cindex Toolbar follow mode
 @cindex Toolbar disabling
+@cindex Toolbar button enablers
 @cindex Proof script indentation
 @cindex Indentation
 @cindex Remote shell
@@ -1701,6 +1710,23 @@ NB: the toolbar is only available with XEmacs.
 The default value is @code{nil}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-toolbar-use-enablers
+@defopt proof-toolbar-use-enablers 
+If non-nil, toolbars buttons may be enabled/disabled automatically.@*
+Toolbar buttons can be automatically enabled/disabled according to
+the context.  Set this variable to nil if you don't like this feature
+or if you find it unreliable.
+
+Notes: 
+* Toolbar enablers are only available with XEmacs 21 and later.
+* With this variable nil, buttons do nothing when they would
+otherwise be disabled.
+* If you change this variable it will only be noticed when you 
+next start Proof General.
+
+The default value is @code{t}.
+@end defopt
+
 
 @c TEXI DOCSTRING MAGIC: proof-toolbar-follow-mode
 @defopt proof-toolbar-follow-mode 
@@ -2480,7 +2506,8 @@ including highlighting, etc.
 
 @c TEXI DOCSTRING MAGIC: proof-terminal-char
 @defvar proof-terminal-char 
-Character which terminates a command in a script buffer.
+Character which terminates a command in a script buffer.@*
+You must set this variable.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-comment-start
 @defvar proof-comment-start 
@@ -2508,7 +2535,7 @@ Matches a save command
 Regexp which matches a command to save a named theorem.@*
 Match number 2 should be the name of the theorem saved.
 Used for setting names of goal..save regions and for default
-@code{func-menu} configuration in proof-script-find-next-goalsave.
+@code{function-menu} configuration in @code{proof-script-find-next-entity}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-goal-command-regexp
 @defvar proof-goal-command-regexp 
@@ -2519,7 +2546,7 @@ Matches a goal command.
 Regexp which matches a command used to issue and name a goal.@*
 Match number 2 should be the name of the goal issued.
 Used for setting names of goal..save regions and for default
-@code{func-menu} configuration in proof-script-find-next-goalsave.
+@code{function-menu} configuration in @code{proof-script-find-next-entity}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps
 @defvar proof-script-next-entity-regexps 
@@ -2565,7 +2592,7 @@ work for goal..saves is calculated from @code{proof-goal-with-hole-regexp},
 @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} of the proof assistant does not support nested goals.
+to @samp{nil} if the proof assistant does not support nested goals.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-count-undos-fn
 @defvar proof-count-undos-fn 
@@ -2594,7 +2621,9 @@ This is used to handle nested goals allowed by some provers.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-state-preserving-p
 @defvar proof-state-preserving-p 
-A predicate, non-nil if its argument (a command) preserves the proof state.
+A predicate, non-nil if its argument (a command) preserves the proof state.@*
+If set, used by @code{proof-execute-minibuffer-cmd} to filter out scripting
+commands which should be entered directly into the script itself.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-activate-scripting-hook
 @defvar proof-activate-scripting-hook 
@@ -2660,19 +2689,39 @@ group.  This allows different proof assistants to coexist
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-init-cmd
 @defvar proof-shell-init-cmd 
-The command for initially configuring the proof process.
+The command for initially configuring the proof process.@*
+This command is sent to the process as soon as it starts up,
+perhaps in order to configure it for Proof General or to
+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.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
 @defvar proof-shell-restart-cmd 
-A command for re-initialising the proof process.
+A command for re-initialising the proof process.@*
+The @code{proof-terminal-char} is added on to the end.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd
 @defvar proof-shell-quit-cmd 
-A command to quit the proof process.  If nil, send EOF instead.
+A command to quit the proof process.  If nil, send EOF instead.@*
+The @code{proof-terminal-char} is added on to the end.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-cd
 @defvar proof-shell-cd 
-Command to the proof assistant to change the working directory.
+Command to the proof assistant to change the working directory.@*
+The format character %s is replaced with the directory, and the
+@code{proof-terminal-char} is added on to the end.
+
+This is used to define the function @code{proof-cd} which 
+changes to the value of (@code{default-directory}) for script buffers.
+For files, the value of (@code{default-directory}) is simply the
+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.
 @end defvar
 
 @node Settings for matching output from proof process
@@ -2715,6 +2764,9 @@ this regexp.  Moreover, an error message should not be matched as an
 eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it
 will be lost.
 
+Error messages are considered to begin from @code{proof-shell-error-regexp}
+and continue until the next prompt.
+
 The engine matches interrupts before errors, see proof-shell-interupt-regexp.
 
 It is safe to leave this variable unset (as nil).
@@ -2816,7 +2868,7 @@ A pair (@var{regexp} . @var{function}) to match a processed file name.
 
 If @var{regexp} matches output, then the function @var{function} is invoked on the
 output string chunk. It must return a script file name (with complete
-path) the system is currently processing. In practice, @var{function} is
+path) the system has successfully processed. In practice, @var{function} is
 likely to inspect the match data.  If it returns the empty string,
 the file name of the scripting buffer is used instead.  If it
 returns nil, no action is taken.
@@ -2828,7 +2880,7 @@ name is added to the front of @samp{@code{proof-included-files-list}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp
 @defvar proof-shell-retract-files-regexp 
-A @var{regexp} to match that the prover has retracted across file boundaries.
+Matches a message that the prover has retracted a file.
 
 At this stage, Proof General's view of the processed files is out of
 date and needs to be updated with the help of the function
@@ -2987,7 +3039,8 @@ processes a file and retracts across file boundaries. The variable
 @c TEXI DOCSTRING MAGIC: proof-included-files-list
 @defvar proof-included-files-list 
 List of files currently included in proof process.@*
-This list contains files in canonical truename format.
+This list contains files in canonical truename format
+(see @samp{@code{file-truename}}).
 
 Whenever a new file is being processed, it gets added to this list
 via the @code{proof-shell-process-file} configuration settings.
@@ -3000,8 +3053,10 @@ Proof General itself will automatically add the filenames of script
 buffers which are completely read, when scripting is deactivated or
 switched to another buffer.
 
-Currently there is no generic provision for removing files which
-are only partly read-in due to an error.
+NB: Currently there is no generic provision for removing files which
+are only partly read-in due to an error, so ideally the proof assistant
+should only output a processed message when a file has been successfully
+read.
 @end defvar
 
 @vindex proof-shell-process-file
@@ -3162,7 +3217,8 @@ Symbol indicating the type of this buffer: @code{'script}, @code{'shell}, or @co
 @c TEXI DOCSTRING MAGIC: proof-included-files-list
 @defvar proof-included-files-list 
 List of files currently included in proof process.@*
-This list contains files in canonical truename format.
+This list contains files in canonical truename format
+(see @samp{@code{file-truename}}).
 
 Whenever a new file is being processed, it gets added to this list
 via the @code{proof-shell-process-file} configuration settings.
@@ -3175,8 +3231,10 @@ Proof General itself will automatically add the filenames of script
 buffers which are completely read, when scripting is deactivated or
 switched to another buffer.
 
-Currently there is no generic provision for removing files which
-are only partly read-in due to an error.
+NB: Currently there is no generic provision for removing files which
+are only partly read-in due to an error, so ideally the proof assistant
+should only output a processed message when a file has been successfully
+read.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-shell-proof-completed
@@ -3221,7 +3279,7 @@ important one is @code{proof-init-segmentation}.
 @defun proof-init-segmentation 
 Initialise the queue and locked spans in a proof script buffer.@*
 Allocate spans if need be.  The spans are detached from the
-buffer, so the locked region is made empty by this function.
+buffer, so the regions are made empty by this function.
 @end defun
 
 For locking files loaded by a proof assistant, we use the next function.
@@ -3251,26 +3309,24 @@ buffer.  This may involve switching from one scripting buffer to
 another.
 
 @c TEXI DOCSTRING MAGIC: proof-activate-scripting
-@defun proof-activate-scripting 
-Activate scripting for the current script buffer.
+@defun proof-activate-scripting &optional nosaves
+Ready prover and activate scripting for the current script buffer.
 
-The current buffer is prepared for scripting.  No changes are
+The current buffer is prepared for scripting. No changes are
 necessary if it is already in Scripting minor mode. Otherwise, it
-will become the current scripting buffer provided the current
-scripting buffer has either no locked region or everything in it has
-been processed.
+will become the new active scripting buffer, provided scripting
+can be switched off in the previous active scripting buffer
+with @samp{@code{proof-deactivate-scripting}}.
 
-If we're changing scripting buffer and the old one is associated with
-a file, add it to @code{proof-included-files-list}.
+Activating a new script buffer may be a good time to ask if the 
+user wants to save some buffers; this is done if the user
+option @samp{@code{proof-query-file-save-when-activating-scripting}} is set
+and provided the optional argument @var{nosaves} is non-nil.
 
-When a new script buffer has scripting minor mode turned on,
-the hooks @samp{@code{proof-activate-scripting-hook}} are run.  This can
-be a useful place to configure the proof assistant for
+Finally, the hooks @samp{@code{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.
 @end defun
 
 The next function is the main one used for parsing the proof script
@@ -3352,10 +3408,35 @@ proof assistant exits, we use the functions
 @code{proof-script-remove-all-spans-and-deactivate}.
 
 @c TEXI DOCSTRING MAGIC: proof-deactivate-scripting
-@deffn Command proof-deactivate-scripting 
-Deactivate scripting, if the current script buffer is active.@*
+@deffn Command proof-deactivate-scripting &optional forcedaction
+Deactivate scripting for the active scripting buffer.
+
 Set @code{proof-script-buffer} to nil and turn off the modeline indicator.
-If the locked region doesn't cover the entire file, retract it.
+No action if there is no active scripting buffer.  
+
+We make sure that the active scripting buffer either has no locked
+region or everything in it has been processed. This is done by
+prompting the user or by automatically taking the action indicated in
+the user option @samp{@code{proof-auto-action-when-deactivating-scripting}.}
+
+If the scripting buffer is (or has become) fully processed, and
+it is associated with a file, it is registered on 
+@samp{@code{proof-included-files-list}}.  Conversely, if it is (or has become)
+empty, make sure that it is @strong{not} registered.  This is to
+make sure that the included files list behaves as we might expect
+with respect to the active scripting buffer, in an attempt to 
+harmonize mixed scripting and file reading in the prover.
+
+This function either succeeds, fails because the user 
+refused to process or retract a partly finished buffer,
+or gives an error message because retraction or processing failed.
+If this function succeeds, then proof-script-buffer=nil afterwards.
+
+The optional argument @var{forcedaction} overrides the user option
+@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents
+questioning the user.  It is used to make a value for
+the @code{kill-buffer-hook} for scripting buffers, so that when
+a scripting buffer is killed it is always retracted.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-restart-buffers
@@ -3477,6 +3558,9 @@ Clear script buffers and send @code{proof-shell-restart-cmd}.@*
 All locked regions are cleared and the active scripting buffer
 deactivated.  
 
+If the proof shell is busy, an interrupt is sent with
+@code{proof-interrupt-process} and we wait until the process is ready. 
+
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
 process.  
@@ -3527,7 +3611,8 @@ action list directly.
 @c TEXI DOCSTRING MAGIC: proof-shell-invisible-command
 @defun proof-shell-invisible-command cmd &optional wait
 Send @var{cmd} to the proof process.@*
-If optional @var{wait} command is non-nil, wait for processing to finish
+By default, let the command be processed asynchronously.
+But if optional @var{wait} command is non-nil, wait for processing to finish
 before and after sending the command.
 @end defun
 
@@ -3624,11 +3709,11 @@ or the last urgent message (position of
 @code{proof-shell-urgent-message-marker}), whichever is later.  
 For example, in this case:
 @lisp
- @var{prompt} @var{input}
+ PROMPT> @var{input}
  @var{output-1}
  @var{urgent-message}
  @var{output-2}
- @var{prompt}
+ PROMPT>
 @end lisp
 @code{proof-marker} is set after @var{input} by @code{proof-shell-insert} and
 @code{proof-shell-urgent-message-marker} is set after @var{urgent-message}.
@@ -3642,7 +3727,7 @@ The first time that a prompt is seen, @code{proof-marker} is
 initialised to the end of the prompt.  This should
 correspond with initializing the process.  The 
 ordinary output before the first prompt is ignored (urgent messages, 
-however, are always processed).
+however, are always processed; hence their name).
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-shell-filter-process-output