Add documentation for proof-shell-trace-output-regexp (Trac #432) and

proof-shell-interactive-prompt-regexp (ref Trac #430)

1 files changed, 42 insertions, 5 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 496d4945..0c62973d 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1657,6 +1657,10 @@ This is an important setting.  Output between @samp{@code{proof-shell-start-goal
 and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
 and possibly analysed further for proof-by-pointing markup.
 If it is left as nil, the goals buffer will not be used.
+
+The goals display starts at the beginning of the match on this
+regexp, unless it has a match group, in which case it starts
+at (@code{match-end} 1).
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
 @defvar proof-shell-end-goals-regexp 
@@ -1665,10 +1669,10 @@ This allows a shorter form of the proof state output to be displayed,
 in case several messages are combined in a command output.
 
 The portion treated as the goals output will be that between the
-@strong{end} of the match on @samp{@code{proof-shell-start-goals-regexp}} and the
-@strong{start} of the match on @samp{@code{proof-shell-end-goals-regexp}}.
+match on @samp{@code{proof-shell-start-goals-regexp}} (which see) and the
+start of the match on @samp{@code{proof-shell-end-goals-regexp}}.
 
-If nil, use the whole of the output after
+If nil, use the whole of the output from the match on
 @samp{@code{proof-shell-start-goals-regexp}} up to the next prompt.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp
@@ -1692,8 +1696,9 @@ during proof, Proof General can consider certain messages to be
 normally supress the output, waiting until the final message appears
 before displaying anything to the user.  Urgent messages escape this:
 typically they include messages that the prover wants the user to
-notice, for example, perhaps, file loading messages, or timing
-statistics.
+notice, for example, perhaps, file loading messages, timing
+statistics or dedicated tracing messages which can be sent to the
+@code{*trace*} buffer.
 
 So that Proof General notices, these urgent messages should be marked-up
 with "eager" annotations.
@@ -1781,6 +1786,37 @@ This feature is useful to give the prover more control over what output
 is shown to the user.  Set to nil to disable.
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-shell-interactive-prompt-regexp
+@defvar proof-shell-interactive-prompt-regexp 
+Matches output from the prover which indicates an interactive prompt.@*
+If we match this, we suppose that the prover has switched to an
+interactive diagnostic mode which requires direct interaction
+with the shell rather than via script management.  In this case,
+the shell buffer will be displayed and the user left to their own
+devices.
+
+Note: this should match a string which is bounded by matches
+on @samp{@code{proof-shell-eager-annotation-start}} and
+@samp{@code{proof-shell-eager-annotation-end}}.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-shell-trace-output-regexp
+@defvar proof-shell-trace-output-regexp 
+Matches tracing output which should be displayed in trace buffer.@*
+Each line which matches this regexp but would otherwise be treated
+as an ordinary response, is sent to the trace buffer instead of the
+response buffer.
+
+This is intended for unusual debugging output from
+the prover, rather than ordinary output from final proofs.
+
+This should match a string which is bounded by matches
+on @samp{@code{proof-shell-eager-annotation-start}} and
+@samp{@code{proof-shell-eager-annotation-end}}.
+
+Set to nil to disable.
+@end defvar
+
 @c TEXI DOCSTRING MAGIC: proof-shell-set-elisp-variable-regexp
 @defvar proof-shell-set-elisp-variable-regexp 
 Matches output telling Proof General to set some variable.@*
@@ -1910,6 +1946,7 @@ scripting (to do undo operations), the whole history is discarded.
 
 
 
+
 @node Hooks and other settings
 @section Hooks and other settings