diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 5 | ||||
| -rw-r--r-- | generic/proof-config.el | 7 |
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 |