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 | |
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')
-rw-r--r-- | generic/proof-config.el | 13 | ||||
-rw-r--r-- | generic/proof-script.el | 8 |
2 files changed, 12 insertions, 9 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index f93235d4..cf090aa1 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -51,7 +51,7 @@ ;; ;; i. When adding a new configuration variable, please ;; (a) put it in the right customize group, and -;; (b) add a magical comment in ProofGeneral.texi/PG-Adapting.texi +;; (b) add a magical comment in ProofGeneral.texi/PG-adapting.texi ;; ;; ii. Presently the customize library seems a bit picky over the ;; :type property and some correct but complex types don't work: @@ -667,6 +667,17 @@ assistant, for example, to compile a completed file." :type '(repeat function) :group 'proof-script) +(defcustom 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 the choice to fully retract the active buffer before +starting scripting in a different buffer. This last behavior is +needed for Coq." + :type 'boolean + :group 'proof-script) + (defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --" "Matches text within a comment telling Proof General to evaluate some code. This allows Emacs Lisp to be executed during scripting. 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 |