diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 85247eda..0028022b 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1883,13 +1883,15 @@ This is an experimental feature, currently work-in-progress." :group 'proof-shell) (defcustom proof-shell-spill-output-regexp nil - "Regexp matching output which is to be ``spilled'' into new buffer. -This allows the prover to output tracing messages, and the like, -into a new buffer. The end of the spilled output is the next -prompt. This is intended for unusual debugging output from the -prover, rather than ordinary output from final proofs. + "Regexp matching tracing output which is ``spilled'' into 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. + Set to nil to disable. -This is an experimental feature, currently work-in-progress." :type '(choice nil regexp) :group 'proof-shell) |