diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2006-09-24 15:05:35 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2006-09-24 15:05:35 +0000 |
| commit | c564bc93d68696dd6b1dc44933e23c1d24656e94 (patch) | |
| tree | c890d44e7944433bdfd2b7afedde3674e37f086e /doc | |
| parent | a744114658a01e46f16eec510e313b72da532aa0 (diff) | |
Add buffer history browsing
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 8c78919a..bb1a7d8d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2833,6 +2833,16 @@ Otherwise the response buffer will accumulate output from the prover. The default value is @code{t}. @end defopt +@c TEXI DOCSTRING MAGIC: proof-keep-response-history +@defopt proof-keep-response-history +Whether to keep a browsable history of responses.@* +With this feature enabled, the buffers used for prover responses will have a +history that can be browsed without processing/undoing in the prover. +(Changes to this variable take effect after restarting the prover). + +The default value is @code{nil}. +@end defopt + @c TEXI DOCSTRING MAGIC: proof-show-debug-messages @defopt proof-show-debug-messages Whether to display debugging messages in the response buffer.@* |