diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-14 15:50:47 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-14 15:50:47 +0000 |
| commit | 05f9272860f9f57e6adfa150734ea7aa29702ca7 (patch) | |
| tree | 2f26bec12453529d2e89efa31dcbf2ae75b2302c /generic/proof-script.el | |
| parent | a2ba24cc1172258abd98eee6350cdb672e50e4de (diff) | |
- move proof-no-fully-processed-buffer to generic/proof-config
- add documentation for it
- add a test case demonstrating it in
coq/ex/test-cases/retract-completely-asserted
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 2c2c760d..2db38563 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -969,14 +969,6 @@ retracted using `proof-auto-retract-dependencies'." ;; taken when scripting is turned off/on. ;; -(defconst proof-no-fully-processed-buffer nil - "Set to t if buffers should always retract before scripting elsewhere. -Leave at nil if fully processd buffers make sense for the current proof -assistant. If nil the user can choose to fully assert a buffer when -starting scripting in a different buffer. If t there is only to choice -to fully retract the active buffer before starting scripting in a different -buffer. This last behavior is needed for Coq.") - (defun proof-protected-process-or-retract (action &optional buffer) "If ACTION='process, process, If ACTION='retract, retract. Process or retract the current buffer, which should be the active |