From c564bc93d68696dd6b1dc44933e23c1d24656e94 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 24 Sep 2006 15:05:35 +0000
Subject: Add buffer history browsing

---
 doc/ProofGeneral.texi | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc')

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.@*
-- 
cgit v1.2.3