diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-17 17:41:06 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-17 17:41:06 +0000 |
| commit | 69e7264621d7d213fcd27f9c63143e9817ea0d6d (patch) | |
| tree | 8a992e4c205b1da864b917b008b505ff234be832 /generic | |
| parent | f5ac02c634619c6eabb355d0e8f96f3c18ce2cd2 (diff) | |
Add proof-cannot-reopen-processed-files to fix behaviour of multiple files for Isabelle.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 2c80983b..917b0536 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1654,7 +1654,21 @@ setting to good effect. If the proof assistant has more complex file dependencies then you should configure it to communicate with Proof General about the dependencies rather than using this setting." :type 'boolean - :group 'proof-shell) + :group 'proof-shell) ;; not really proof-shell + +(defcustom proof-cannot-reopen-processed-files nil + "Non-nil if the prover allows re-opening of already processed files. + +If the user has used Proof General to process a file incrementally, +then PG will retain the spans recording undo history in the buffer +corresponding to that file (provided it remains visited in Emacs). + +If the prover allows, it will be possible to undo to a position within +this file. If the prover does *not* allow this, this variable should +be set non-nil, so that when a completed file is activated for +scripting (to do undo operations), the whole history is discarded." + :type 'boolean + :group 'proof-shell) ;; not really proof shell ;; (defcustom proof-shell-adjust-line-width-cmd nil |