Document some new settings

1 files changed, 87 insertions, 20 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 0b947589..5bed9953 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -519,7 +519,7 @@ Suggestion: this can be set a function called by @samp{@code{proof-pre-shell-sta
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-mode-for-response
 @defvar proof-mode-for-response 
-Mode for proof response buffer.@*
+Mode for proof response buffer (and trace buffer, if used).@*
 Usually customised for specific prover.
 Suggestion: this can be set a function called by @samp{@code{proof-pre-shell-start-hook}}.
 @end defvar
@@ -646,12 +646,15 @@ defining functions, images.
 @c TEXI DOCSTRING MAGIC: PA-toolbar-entries
 @defvar PA-toolbar-entries 
 List of entries for Proof General toolbar and Scripting menu.@*
-Format of each entry is (@var{token} @var{menuname} @var{tooltip} @var{enabler-p}).
+Format of each entry is (@var{token} @var{menuname} @var{tooltip} @var{dynamic-enabler-p} @var{enable}).
 
 For each @var{token}, we expect an icon with base filename @var{token},
-a function proof-toolbar-<TOKEN>, and (optionally) an enabler 
+a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler 
 proof-toolbar-<TOKEN>-enable-p.
 
+If @var{enablep} is absent, item is enabled; if @var{enablep} is present, item
+is only added to menubar and toolbar if @var{enablep} is non-null.
+
 If @var{menuname} is nil, item will not appear on the scripting menu.
 
 If @var{tooltip} is nil, item will not appear on the toolbar.
@@ -986,6 +989,20 @@ and @samp{@code{proof-generic-count-undos}}.  If you don't use those,
 may be left as nil.
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-undo-n-times-cmd
+@defvar proof-undo-n-times-cmd 
+Command to undo n steps of the currently open goal.@*
+String or function.
+If this is set to a string, @samp{%s} will be replaced by the number of
+undo steps to issue. 
+If this is set to a function, it should return the appropriate
+command when called with an integer (the number of undo steps).
+
+This setting is used for the default @samp{@code{proof-generic-count-undos}}.
+If you set @samp{@code{proof-count-undos-fn}} to some other function, there is no
+need to set this variable.
+@end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count
 @defvar proof-ignore-for-undo-count 
 Matcher for script commands to be ignored in undo count.@*
@@ -1017,6 +1034,11 @@ For this function to work properly, you must configure
 @samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}.
 @end defun
 
+
+
+
+
+
 @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.@*
@@ -1028,9 +1050,6 @@ of definitions, declarations, or whatever.
 
 The special string @code{proof-no-command} means there is nothing to do.
 
-Important: the generic implementation @samp{@code{proof-generic-find-and-forget}}
-does nothing, it always returns @samp{@code{proof-no-command}}.
-
 This is an important function for script management.
 Study one of the existing instantiations for examples of how to write it,
 or leave it set to the default function @samp{@code{proof-generic-find-and-forget}}
@@ -1044,13 +1063,25 @@ This is a long-range forget: we know that there is no
 open goal at the moment, so forgetting involves unbinding
 declarations, etc, rather than undoing proof steps.
 
-Currently this has a trivial implementation: it 
-just returns @code{proof-no-command}, meaning @samp{do nothing}.
+This generic implementation assumes it is enough to find the 
+nearest following span with a @samp{name} property, and retract
+that using @samp{@code{proof-forget-id-command}} with the given name.
 
-Check the @code{lego-find-and-forget} or @code{coq-find-and-forget}
-functions for examples of how to write this function.
+If this behaviour is not correct, you must customize the function
+with something different.
 @end defun
 
+@c TEXI DOCSTRING MAGIC: proof-forget-id-command
+
+
+@defvar proof-forget-id-command 
+Command to forget back to a given named span.@*
+A string; @samp{%s} will be replaced by the name of the span.
+
+This is only used in the implementation of @samp{@code{proof-generic-find-and-forget}},
+you only need to set if you use that function (by not customizing
+@samp{@code{proof-find-and-forget-fn}}.
+@end defvar
 @c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn
 @defvar proof-goal-hyp-fn 
 Function which returns cons cell if point is at a goal/hypothesis.@*
@@ -1070,6 +1101,7 @@ You must set this (perhaps to a no-op) for script management to work.
 @end defvar
 
 
+
 @node Nested proofs
 @section Nested proofs
 
@@ -1457,6 +1489,12 @@ into tokens for the proof assistant.
 @node Settings for matching various output from proof process
 @section Settings for matching various output from proof process
 
+These settings control the way Proof General reacts to process output.
+The single most important setting is
+@code{proof-shell-annotated-prompt-regexp}, which @b{must} be set as
+part of the prover configuraton.  This is used to configure the
+communication with the prover process.
+
 
 @c TEXI DOCSTRING MAGIC: proof-shell-wakeup-char
 @defvar proof-shell-wakeup-char 
@@ -1478,12 +1516,18 @@ You don't really need to set it.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp
 @defvar proof-shell-annotated-prompt-regexp 
-Regexp matching a (possibly annotated) prompt pattern.@*
-Output is grabbed between pairs of lines matching this regexp.
-To help matching you may be able to annotate the proof assistant
-prompt with a special character not appearing in ordinary output.
-The special character should appear in this regexp, and should
-be the value of @code{proof-shell-wakeup-char}.
+Regexp matching a (possibly annotated) prompt pattern.
+
+@var{this} IS THE @var{most} @var{important} @var{setting} TO @var{configure}!!   
+
+Output is grabbed between pairs of lines matching this regexp,
+and the appearance of this regexp is used by Proof General to
+recognize when the prover has finished processing a command.
+
+To help speed up matching you may be able to annotate the 
+proof assistant prompt with a special character not appearing 
+in ordinary output.  The special character should appear in 
+this regexp, and should be the value of @code{proof-shell-wakeup-char}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-abort-goal-regexp
 @defvar proof-shell-abort-goal-regexp 
@@ -1500,7 +1544,9 @@ 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.
+and continue until the next prompt.  The variable
+@samp{@code{proof-shell-truncate-before-error}} controls whether text before the
+error message is displayed.
 
 The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}.
 
@@ -1519,6 +1565,21 @@ The engine matches interrupts before errors, see @code{proof-shell-error-regexp}
 
 It is safe to leave this variable unset (as nil).
 @end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-shell-truncate-before-error
+@defvar proof-shell-truncate-before-error 
+Non-nil means truncate output that appears before error messages.@*
+If nil, the whole output that the prover generated before the last
+error message will be shown.
+
+NB: the default setting for this is @samp{t} to be compatible with
+behaviour in Proof General before version 3.4.  The more obvious
+setting for new instances is probably @samp{nil}.
+
+Interrupt messages are treated in the same way.
+See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt-regexp}}.
+@end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp
 @defvar proof-shell-proof-completed-regexp 
 Regexp matching output indicating a finished proof.
@@ -1771,6 +1832,7 @@ shell variables:
    @code{proof-mode-for-shell}
    @code{proof-mode-for-response}
    @code{proof-mode-for-goals}
+   @code{proof-shell-trace-output-regexp}
 @end lisp
 This is the bare minimum needed to get a shell buffer and
 its friends configured in the function @code{proof-shell-start}.
@@ -2106,12 +2168,16 @@ will magically restore the commas to the default font for you.
 
 The hack is rather painful and forces immediate fontification of
 files on loading (no lazy, caching locking).  It is unreliable
-under GNU Emacs, to boot.
+under FSF Emacs, to boot.
 
 @var{lego} and Coq enable it by tradition.
 @end defvar
 
-
+@c TEXI DOCSTRING MAGIC: proof-before-fontify-output-hook
+@defvar proof-before-fontify-output-hook 
+This hook is called before fonfitying a region in an output buffer.@*
+This hook is mainly used by @code{phox-sym-lock}.
+@end defvar
 
 
 @node Configuring X-Symbol
@@ -3314,7 +3380,8 @@ Only @var{output-2} will be processed.  For this reason, error
 messages and interrupt messages should @strong{not} be considered
 urgent messages.
 
-Output is processed using @code{proof-shell-filter-process-output}.
+Output is processed using the function
+@samp{@code{proof-shell-filter-process-output}}.
 
 The first time that a prompt is seen, @code{proof-marker} is 
 initialised to the end of the prompt.  This should