diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-09-04 17:21:47 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-09-04 17:21:47 +0000 |
| commit | cbbe19911ca15dd6466e91d6fb7c135e6e32c393 (patch) | |
| tree | 67adbed6bab757467ff6cc74771adf8d15ff5d1d /generic/proof.el | |
| parent | 79d0ea0d7b2f205d0cc8224f93b7b43dbef00ec7 (diff) | |
Add proof-thms-buffer
Diffstat (limited to 'generic/proof.el')
| -rw-r--r-- | generic/proof.el | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/generic/proof.el b/generic/proof.el index 9edd72d3..6c93b7af 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -66,6 +66,7 @@ read.") (defvar proof-script-buffer nil "The currently active scripting buffer or nil if none.") +;; FIXME: should fixup Coq's multiple file mode (defvar proof-previous-script-buffer nil "Previous value of proof-script-buffer, recorded when scripting turned off. At the moment, this is only used for Coq's ugly multiple file code, @@ -84,6 +85,10 @@ to help guess the directory of files Coq says it's reinterning.") "A tracing buffer for storing tracing output from the proof shell. See `proof-shell-trace-output-regexp' for details.") +(defvar proof-thms-buffer nil + "A buffer for displaying a list of theorems from the proof assistant. +See `proof-shell-thm-display-regexp' for details.") + (defvar proof-shell-error-or-interrupt-seen nil "Flag indicating that an error or interrupt has just occurred. Set to 'error or 'interrupt if one was observed from the proof |