aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1998-11-26 18:29:13 +0000
committerDavid Aspinall1998-11-26 18:29:13 +0000
commit54bdffb11596d5f9083c72690d147662a607ecf9 (patch)
treee14d30fa8152ed4cba52894a126c1b859c2816cf
parent588314e72d2b390da057a30d6aa9b9cdc0f6ef07 (diff)
Added proof-shell-clear-goals-regexp.
-rw-r--r--doc/ProofGeneral.texi5
-rw-r--r--generic/proof-config.el7
2 files changed, 12 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 2d406d94..9910be75 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2433,6 +2433,7 @@ Regexp matching output indicating a finished proof.
Regexp matching output telling Proof General to clear the response buffer.
This feature is useful to give the prover more control over what output
is shown to the user. Set to nil to disable.
+@c TEXI DOCSTRING MAGIC: proof-shell-clear-goals-regexp
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp
@defvar proof-shell-start-goals-regexp
@@ -3244,6 +3245,10 @@ Ordinary output is only displayed when the proof action list
becomes empty, to avoid a confusing rapidly changing output.
@end defun
+@c TEXI DOCSTRING MAGIC: proof-shell-filter-process-output
+
+
+
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 67deb0e4..636f1f1f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -752,6 +752,13 @@ is shown to the user. Set to nil to disable."
:type 'regexp
:group 'proof-shell)
+(defcustom proof-shell-clear-goals-regexp nil
+ "Regexp matching output telling Proof General to clear the goals buffer.
+This feature is useful to give the prover more control over what output
+is shown to the user. Set to nil to disable."
+ :type 'regexp
+ :group 'proof-shell)
+
(defcustom proof-shell-start-goals-regexp ""
"Regexp matching the start of the proof state output."
:type 'regexp