From 05f9272860f9f57e6adfa150734ea7aa29702ca7 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 14 Jan 2011 15:50:47 +0000 Subject: - 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 --- generic/proof-script.el | 8 -------- 1 file changed, 8 deletions(-) (limited to 'generic/proof-script.el') 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 -- cgit v1.2.3