diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 29 | ||||
| -rw-r--r-- | 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))) |