From 2b12ea7260cf8fc3301d75f60fbf69288ecd09ad Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 18 Jun 2002 23:08:53 +0000
Subject: Remove global testing and lift-global function; rename
 proof-nested-goals -> proof-nested-goals-history.

---
 generic/proof-config.el | 29 ++---------------------------
 generic/proof-script.el | 13 +++----------
 2 files changed, 5 insertions(+), 37 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index dd1d05b4..c59e4b3c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1158,11 +1158,7 @@ The possibilities are:
     'extend  -  keep extending the closed region until a save or goal.
 
 If your proof assistant allows nested goals, it will be wrong to close
-off the portion of proof so far, so this variable should be set to nil.
-There is no built-in understanding of the undo behaviour of nested
-proofs; instead there is some support for un-nesting nested proofs in
-the proof-lift-global mechanism.  (Of course, this is risky in case of
-nested contexts!)"
+off the portion of proof so far, so this variable should be set to nil."
   :type '(choice
 	  (const :tag "Close on save only" nil)
 	  (const :tag "Close next command" closeany)
@@ -1170,16 +1166,6 @@ nested contexts!)"
 	  (const :tag "Extend" ignore))
   :group 'proof-script)
 
-(defcustom proof-lift-global nil
-  "Function which lifts local lemmas from inside goals out to top level.
-This function takes the local goalsave span as an argument. Leave this
-set this at `nil' if the proof assistant does not support nested goals,
-or if you don't want to write a function to do move them around."
-  :type 'function
-  ;; FIXME customize broken on choices with function in them?
-  ;; :type '(choice (const :tag "No local lemmas" nil) (function))
-  :group 'proof-script)
-
 (defcustom proof-count-undos-fn 'proof-generic-count-undos
   "Function to calculate a command to issue undos to reach a target span.
 The function takes a span as an argument, and should return a string
@@ -1286,8 +1272,7 @@ need to set this variable."
   :type '(or string function)
   :group 'proof-script)
 
-
-(defcustom proof-nested-goals-p nil
+(defcustom proof-nested-goals-history-p nil
   "Whether the prover supports recovery of history for nested proofs.
 If it does, Proof General will retain history inside nested proofs;
 otherwise Proof General will amalgamate nested proofs into single
@@ -1295,16 +1280,6 @@ steps."
   :type 'boolean
   :group 'proof-script)
 
-(defcustom proof-global-p nil
-  "Whether a command is a global declaration.  Predicate on strings or nil.
-This is used to handle nested goals allowed by some provers, by
-recognizing global declarations as candidates for rearranging the
-proof script.
-
-May be left as nil to disable this function."
-  :type 'function
-  :group 'proof-script)
-
 (defcustom proof-state-preserving-p 'proof-generic-state-preserving-p
   "A predicate, non-nil if its argument (a command) preserves the proof state.
 If set, used by proof-minibuffer-cmd to filter out scripting
diff --git a/generic/proof-script.el b/generic/proof-script.el
index c47ee5f0..02ae8624 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1210,7 +1210,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	   ;; and use nested goals mechanism instead.
 	   (funcall proof-really-save-command-p span cmd)
 	   (decf proof-nesting-depth) ;; [always non-nil/true]
-	   (if proof-nested-goals-p
+	   (if proof-nested-goals-history-p
 	       ;; For now, we only support this nesting behaviour: 
 	       ;; don't amalgamate unless the nesting depth is 0,
 	       ;; i.e. we're in a top-level proof.
@@ -1273,7 +1273,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 			   (or (span-property gspan 'nestedundos) 0))))
 		 ;; Increment depth for a nested save, in case
 		 ;; prover supports history of nested proofs
-		 ((and proof-nested-goals-p
+		 ((and proof-nested-goals-history-p
 		       proof-save-command-regexp
 		       (proof-string-match proof-save-command-regexp cmd))
 		  (incf lev))
@@ -1440,14 +1440,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
       (if proof-shell-proof-completed
 	  (incf proof-shell-proof-completed))
       
-      (pg-set-span-helphighlights span)
-
-      ;; FIXME 3.4: probably want to remove this global stuff now,
-      ;; has been removed for Coq.
-      (and proof-global-p 
-	   (funcall proof-global-p cmd)
-	   proof-lift-global
-	   (funcall proof-lift-global span)))))
+      (pg-set-span-helphighlights span))))
 
   ;; State of scripting may have changed now
   (run-hooks 'proof-state-change-hook)))
-- 
cgit v1.2.3