From 4f62e0e371070e8b5302ed240475ffe5e94d5937 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 10 Jan 2012 11:54:36 +0000 Subject: Add documentation for proof-shell-trace-output-regexp (Trac #432) and proof-shell-interactive-prompt-regexp (ref Trac #430) --- doc/PG-adapting.texi | 47 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 5 deletions(-) (limited to 'doc/PG-adapting.texi') 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 -- cgit v1.2.3