- 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

1 files changed, 12 insertions, 1 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.