Improved documentation, more options added

1 files changed, 272 insertions, 112 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index cf38c25d..be90991e 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1690,18 +1690,21 @@ For more help, see @inforef{Easy Customization, ,xemacs}.
 @cindex buffer display customization
 @cindex frames
 @cindex multiple frames
+@cindex three-buffer interaction
 
-If you are working on a workstation with a window system, you can use
-Emacs to manage several @i{frames} on the display, to keep the goals
-buffer displayed in a fixed place on your screen and in a certain font,
-for example.  A convenient way to do this is via
-@code{special-display-regexps}, for example:
+By default, Proof General displays two buffers during scripting, in a
+split window on the display.  One buffer is the script buffer.  The
+other buffer is either the goals buffer (e.g. @code{*isabelle-goals*})
+or the response buffer (@code{*isabelle-response*}).  Proof General
+switches between these last two automatically.
+
+You may prefer to display all three of these buffers at once, if your
+screen is large enough.  This is useful, for example, to see output from
+the @code{proof-find-theorems} command at the same time as the subgoal
+list.  The user option @code{proof-window-dedicated} can be set
+to make Proof General keep both the goals and response buffer
+displayed.
 
-@lisp
-(setq special-display-regexps
-        (cons "\\*Inferior.*-\\(goals\\|response\\)\\*"
-         special-display-regexps))
-@end lisp
 
 
 @c TEXI DOCSTRING MAGIC: proof-auto-delete-windows
@@ -1718,6 +1721,49 @@ The default value is @code{nil}.
 @end defopt
 
 
+@c TEXI DOCSTRING MAGIC: proof-window-dedicated
+@defopt proof-window-dedicated 
+Whether response and goals buffers have dedicated windows.@*
+If non-nil, Emacs windows displaying messages from the prover will not
+be switchable to display other windows.
+
+This option can help manage your display.
+
+Setting this option triggers a three-buffer mode of interaction where
+the goals buffer and response buffer are both displayed, rather than
+the two-buffer mode where they are switched between.  It also prevents
+Emacs automatically resizing windows between proof steps.  
+
+If you use several frames (X windows), you can force a frame to stick
+to showing the goals or response buffer.
+
+For single frame use this option may be inconvenient for
+experienced Emacs users.
+
+The default value is @code{nil}.
+@end defopt
+
+If you are working on a workstation with a window system, you can use
+Emacs to manage several @i{frames} on the display, to keep the goals
+buffer displayed in a fixed place on your screen and in a certain font,
+for example.  A convenient way to do this is via
+@code{special-display-regexps}, for example:
+
+@lisp
+(setq special-display-regexps
+        (cons "\\*isabelle-\\(goals\\|response\\)\\*"
+         special-display-regexps))
+@end lisp
+This setting makes the @code{*isabelle-goals*} and
+@code{*isabelle-response*} buffers automatically create their own
+frames.  The user option @code{proof-auto-delete-windows} may help if
+you make a setting like this.
+
+
+
+
+
+
 
 
 @node User options
@@ -1737,52 +1783,71 @@ The default value is @code{nil}.
 @cindex Running proof assistant remotely
 @c @cindex formatting proof script
 
-Here are the remaining user options for Proof General.  These can be set
-via the customization system, via the old-fashioned @code{M-x
-edit-options} mechanism, or simply by adding @code{setq}'s to your
-@file{.emacs} file.  The first approach is strongly recommended.
+Here are the user options for Proof General (except the two display
+options mentioned above).  These can be set via the customization
+system, via the old-fashioned @code{M-x edit-options} mechanism, or
+simply by adding @code{setq}'s to your @file{.emacs} file.  The first
+approach is strongly recommended.
 
 
-@c TEXI DOCSTRING MAGIC: proof-prog-name-ask
-@defopt proof-prog-name-ask 
-If non-nil, query user which program to run for the inferior process.
+@c TEXI DOCSTRING MAGIC: proof-splash-enable
+@defopt proof-splash-enable 
+If non-nil, display a splash screen when Proof General is loaded.
 
-The default value is @code{nil}.
+The default value is @code{t}.
 @end defopt
 
-@c TEXI DOCSTRING MAGIC: proof-prog-name-guess
-@defopt proof-prog-name-guess 
-If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@*
-This option is compatible with @code{proof-prog-name-ask}.
-No effect if @code{proof-guess-command-line} is nil.
+@c TEXI DOCSTRING MAGIC: proof-electric-terminator-enable
+@defun proof-electric-terminator-enable 
+Make sure the modeline is updated to display new value for electric terminator.
+@end defun
+
+@c TEXI DOCSTRING MAGIC: proof-toolbar-enable
+@deffn Command proof-toolbar-enable 
+Initialize Proof General toolbar and enable it for the current buffer.@*
+If proof-mode-use-toolbar is nil, change the current buffer toolbar
+to the default toolbar.
+@end deffn
+
+@c TEXI DOCSTRING MAGIC: proof-x-symbol-enable
+@defopt proof-x-symbol-enable 
+Whether to use x-symbol in Proof General buffers.@*
+If you activate this variable, whether or not you get x-symbol support
+depends on if your proof assistant supports it and it is enabled
+inside your Emacs.
 
 The default value is @code{nil}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-output-fontify-enable
+@defopt proof-output-fontify-enable 
+Whether to fontify output from the proof assistant.@*
+If non-nil, output from the proof assistant will be highlighted
+in the goals and response buffers.
+(This is providing @code{font-lock-keywords} have been set for the 
+buffer modes).
 
-@c TEXI DOCSTRING MAGIC: proof-rsh-command
-@defopt proof-rsh-command 
-Shell command prefix to run a command on a remote host.  @*
-For example,
+The default value is @code{t}.
+@end defopt
+
+@c TEXI DOCSTRING MAGIC: proof-strict-read-only
+@defopt proof-strict-read-only 
+Whether Proof General is strict about the read-only region in buffers.@*
+If non-nil, an error is given when an attempt is made to edit the
+read-only region.  If nil, Proof General is more relaxed (but may give
+you a reprimand!).
+
+If you change @code{proof-strict-read-only} during a session, you must use
 @lisp
-   ssh bigjobs
+"Restart" (@code{proof-shell-restart})
 @end lisp
-Would cause Proof General to issue the command @samp{ssh bigjobs isabelle}
-to start Isabelle remotely on our large compute server called @samp{bigjobs}.
-
-The protocol used should be configured so that no user interaction
-(passwords, or whatever) is required to get going.
+The default value for @code{proof-strict-read-only} depends on which
+version of Emacs you are using.  In FSF Emacs, strict read only is buggy
+when it used in conjunction with font-lock, so it is disabled by default.
 
-The default value is @code{""}.
+The default value is @code{strict}.
 @end defopt
 
-@c TEXI DOCSTRING MAGIC: proof-toolbar-enable
-@deffn Command proof-toolbar-enable 
-Initialize Proof General toolbar and enable it for the current buffer.@*
-If proof-mode-use-toolbar is nil, change the current buffer toolbar
-to the default toolbar.
-@end deffn
-
 @c TEXI DOCSTRING MAGIC: proof-toolbar-use-button-enablers
 @defopt proof-toolbar-use-button-enablers 
 If non-nil, toolbars buttons may be enabled/disabled automatically.@*
@@ -1800,59 +1865,33 @@ next start Proof General.
 The default value is @code{t}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-auto-retract
+@defopt proof-auto-retract 
+If non-nil, retract automatically when locked region is edited.@*
+With this option active, the locked region will automatically be
+unlocked when the user attempts to edit it.   To make use of this
+option, @code{proof-strict-read-only} should be turned off.
 
-@c TEXI DOCSTRING MAGIC: proof-toolbar-follow-mode
-@defopt proof-toolbar-follow-mode 
-Choice of how point moves with toolbar commands.@*
-One of the symbols: @code{'locked}, @code{'follow}, @code{'ignore}.
-If @code{'locked}, point sticks to the end of the locked region with toolbar commands.
-If @code{'follow}, point moves just when needed to display the locked region end.
-If @code{'ignore}, point is never moved after toolbar movement commands.
-
-The default value is @code{locked}.
-@end defopt
-
-@c TEXI DOCSTRING MAGIC: proof-window-dedicated
-@defopt proof-window-dedicated 
-Whether response and goals buffers have dedicated windows.@*
-If non-nil, Emacs windows displaying messages from the prover will not
-be switchable to display other windows.
-
-This option can help manage your display.
-
-Setting this option triggers a three-buffer mode of interaction where
-the goals buffer and response buffer are both displayed, rather than
-the two-buffer mode where they are switched between.  It also prevents
-Emacs automatically resizing windows between proof steps.  
-
-If you use several frames (X windows), you can force a frame to stick
-to showing the goals or response buffer.
-
-For single frame use this option may be inconvenient for
-experienced Emacs users.
+Note: this feature has not been implemented yet, it is only an idea.
 
 The default value is @code{nil}.
 @end defopt
 
-@c FIXME needs to mention that without dedicated windows, buffers may be 
-@c hidden. Refer to the XEmacs manual on customising buffer display.
+@c TEXI DOCSTRING MAGIC: proof-query-file-save-when-activating-scripting
+@defopt proof-query-file-save-when-activating-scripting 
+If non-nil, query user to save files when activating scripting.
 
-@c TEXI DOCSTRING MAGIC: proof-strict-read-only
-@defopt proof-strict-read-only 
-Whether Proof General is strict about the read-only region in buffers.@*
-If non-nil, an error is given when an attempt is made to edit the
-read-only region.  If nil, Proof General is more relaxed (but may give
-you a reprimand!).
+Often, activating scripting or executing the first scripting command
+of a proof script will cause the proof assistant to load some files
+needed by the current proof script.  If this option is non-nil, the
+user will be prompted to save some unsaved buffers in case any of 
+them corresponds to a file which may be loaded by the proof assistant.
 
-If you change @code{proof-strict-read-only} during a session, you must use
-@lisp
-"Restart" (@code{proof-shell-restart})
-@end lisp
-The default value for @code{proof-strict-read-only} depends on which
-version of Emacs you are using.  In FSF Emacs, strict read only is buggy
-when it used in conjunction with font-lock, so it is disabled by default.
+You can turn this option off if the save queries are annoying, but
+be warned that with some proof assistants this may risk processing 
+files which are out of date with respect to the lodead buffers!
 
-The default value is @code{strict}.
+The default value is @code{t}.
 @end defopt
 
 @c TEXI DOCSTRING MAGIC: proof-script-indent
@@ -1873,39 +1912,60 @@ This option is not fully-functional at the moment.
 The default value is @code{nil}.
 @end defopt
 
-@c TEXI DOCSTRING MAGIC: proof-script-command-separator
-@defopt proof-script-command-separator 
-String separating commands in proof scripts.@*
-For example, if a proof assistant prefers one command per line, then 
-this string should be set to a newline.  Otherwise it should be
-set to a space.
+@c TEXI DOCSTRING MAGIC: proof-prog-name-ask
+@defopt proof-prog-name-ask 
+If non-nil, query user which program to run for the inferior process.
 
-The default value is @code{" "}.
+The default value is @code{nil}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-prog-name-guess
+@defopt proof-prog-name-guess 
+If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@*
+This option is compatible with @code{proof-prog-name-ask}.
+No effect if @code{proof-guess-command-line} is nil.
 
-@c TEXI DOCSTRING MAGIC: proof-splash-enable
-@defopt proof-splash-enable 
-If non-nil, display a splash screen when Proof General is loaded.
+The default value is @code{nil}.
+@end defopt
+
+@c TEXI DOCSTRING MAGIC: proof-tidy-response
+@defopt proof-tidy-response 
+Non-nil indicates that the response buffer should be cleared often.@*
+The response buffer can be set either to accumulate output, or to
+clear frequently.  
+
+With this variable non-nil, the response buffer is kept tidy by
+clearing it often, typically between successive commands (just like the
+goals buffer).  
+
+Otherwise the response buffer will accumulate output from the prover.
 
 The default value is @code{t}.
 @end defopt
 
-@c TEXI DOCSTRING MAGIC: proof-query-file-save-when-activating-scripting
-@defopt proof-query-file-save-when-activating-scripting 
-If non-nil, query user to save files when activating scripting.
+@c TEXI DOCSTRING MAGIC: proof-show-debug-messages
+@defopt proof-show-debug-messages 
+Whether to display debugging messages in the response buffer.@*
+If non-nil, debugging messages are displayed in the response giving
+information about what Proof General is doing.
+To avoid erasing the messages shortly after they're printed, 
+you should set @samp{@code{proof-tidy-response}} to nil.
 
-Often, activating scripting or executing the first scripting command
-of a proof script will cause the proof assistant to load some files
-needed by the current proof script.  If this option is non-nil, the
-user will be prompted to save some unsaved buffers in case any of 
-them corresponds to a file which may be loaded by the proof assistant.
+The default value is @code{t}.
+@end defopt
 
-You can turn this option off if the save queries are annoying, but
-be warned that with some proof assistants this may risk processing 
-files which are out of date with respect to the lodead buffers!
 
-The default value is @code{t}.
+@c ******* NON-BOOLEANS *******
+
+@c TEXI DOCSTRING MAGIC: proof-toolbar-follow-mode
+@defopt proof-toolbar-follow-mode 
+Choice of how point moves with toolbar commands.@*
+One of the symbols: @code{'locked}, @code{'follow}, @code{'ignore}.
+If @code{'locked}, point sticks to the end of the locked region with toolbar commands.
+If @code{'follow}, point moves just when needed to display the locked region end.
+If @code{'ignore}, point is never moved after toolbar movement commands.
+
+The default value is @code{locked}.
 @end defopt
 
 @c TEXI DOCSTRING MAGIC: proof-auto-action-when-deactivating-scripting
@@ -1930,6 +1990,33 @@ is no locked region.
 The default value is @code{nil}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-script-command-separator
+@defopt proof-script-command-separator 
+String separating commands in proof scripts.@*
+For example, if a proof assistant prefers one command per line, then 
+this string should be set to a newline.  Otherwise it should be
+set to a space.
+
+The default value is @code{" "}.
+@end defopt
+
+@c TEXI DOCSTRING MAGIC: proof-rsh-command
+@defopt proof-rsh-command 
+Shell command prefix to run a command on a remote host.  @*
+For example,
+@lisp
+   ssh bigjobs
+@end lisp
+Would cause Proof General to issue the command @samp{ssh bigjobs isabelle}
+to start Isabelle remotely on our large compute server called @samp{bigjobs}.
+
+The protocol used should be configured so that no user interaction
+(passwords, or whatever) is required to get going.
+
+The default value is @code{""}.
+@end defopt
+
+
 
 
 @node Changing faces
@@ -3210,6 +3297,61 @@ Regexp matching end of output from the prover after pbp commands.@*
 In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}.
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-shell-start-char
+@defvar proof-shell-start-char 
+Starting special for a subterm markup.@*
+Subsequent characters with values @strong{below} @code{proof-shell-first-special-char}
+are assumed to be subterm position indicators.  Subterm markups should
+be finished with @code{proof-shell-end-char}.
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-end-char
+@defvar proof-shell-end-char 
+Finishing special for a subterm markup.@*
+See documentation of @code{proof-shell-start-char}.
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-goal-char
+@defvar proof-shell-goal-char 
+goal mark
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-field-char
+@defvar proof-shell-field-char 
+annotated field end
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-start-char
+@defvar proof-shell-start-char 
+Starting special for a subterm markup.@*
+Subsequent characters with values @strong{below} @code{proof-shell-first-special-char}
+are assumed to be subterm position indicators.  Subterm markups should
+be finished with @code{proof-shell-end-char}.
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-end-char
+@defvar proof-shell-end-char 
+Finishing special for a subterm markup.@*
+See documentation of @code{proof-shell-start-char}.
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-goal-char
+@defvar proof-shell-goal-char 
+goal mark
+@end defvar
+@c TEXI DOCSTRING MAGIC: proof-shell-field-char
+@defvar proof-shell-field-char 
+annotated field end
+@end defvar
+
+
+The final setting just configures where the ``proof completed''
+message appears. 
+@c TEXI DOCSTRING MAGIC: proof-goals-display-qed-message
+@defvar proof-goals-display-qed-message 
+If non-nil, display the proof-completed message in the goals buffer.@*
+For some proof assistants (e.g. Isabelle) it seems aesthetic to
+display the QED message in the goals buffer, even though it doesn't
+contain any goals and shouldn't be marked up for proof-by-pointing.
+
+If this setting is non-nil, QED messages appear in the goals
+buffer.  Otherwise they appear in the response buffer.
+@end defvar
+
 
 
 @node Global constants
@@ -3377,8 +3519,8 @@ for a automatic approximation to multiple file handling.
 
 
 
-@node Configuring X-Symbol::
-@section Configuring X-Symbol::
+@node Configuring X-Symbol
+@section Configuring X-Symbol
 @cindex X-Symbol
 
 The X-Symbol package (by Christoph Wedler) displays characters from a
@@ -3408,8 +3550,16 @@ several variables that Proof General uses to configure X-Symbol with.
 @code{@var{myprover}sym-font-lock-keywords}
 
 @c TEXI DOCSTRING MAGIC: proof-xsym-activate-command
+@defvar proof-xsym-activate-command 
+Not documented.
+@end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command
+@defvar proof-xsym-deactivate-command 
+Command to deactivate token input/output for X-Symbol.@*
+If non-nil, this command is sent to the proof assistant when 
+X-Symbol support is deactivated.
+@end defvar
 
 We expect tokens to be used uniformly, so that along with each script
 mode buffer, the response buffer, goals buffer, and shell buffer are all
@@ -3418,6 +3568,14 @@ automatically.  If you want additional modes, you can set
 @code{proof-xsym-extra-modes}.
 
 @c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes
+@defvar proof-xsym-extra-modes 
+List of additional mode names to use X-Symbol with Proof General tokens.@*
+These modes will have X-Symbol enabled for the proof assistant token language,
+in addition to the four modes for Proof General (script, shell, response, pbp).
+
+Set this variable if you want additional modes to also display 
+tokens (for example, editing documentation or source code files).
+@end defvar
 
 
 
@@ -4114,8 +4272,10 @@ Marker in proof shell buffer pointing to end of last urgent message.
 @c TEXI DOCSTRING MAGIC: proof-shell-process-urgent-message
 @defun proof-shell-process-urgent-message message
 Analyse urgent @var{message} for various cases.@*
-Included file, retracted file, cleared response buffer, or
-if none of these apply, display.
+Cases are: included file, retracted file, cleared response buffer, or
+if none of these apply, display it.
+@var{message} should be a string annotated with 
+@code{proof-shell-eager-annotation-start}, @code{proof-shell-eager-annotation-end}.
 @end defun
 
 The main processing point which triggers other actions is