diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | generic/proof-script.el | 24 |
2 files changed, 30 insertions, 7 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index de396c53..f54363a4 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1019,6 +1019,13 @@ may be left as nil." :type '(choice nil regexp) :group 'proof-script) +;; FIXME: doc this next one. +(defcustom proof-nested-undo-regexp nil + "Regexp for commands that must be counted in nested goal-save regions. +Used for provers which allow nested-goal saves but a flat history." + :type '(choice nil regexp) + :group 'proof-script) + (defcustom proof-ignore-for-undo-count nil "Matcher for script commands to be ignored in undo count. May be left as nil, in which case it will be set to @@ -1274,8 +1281,10 @@ need to set this variable." (defcustom proof-nested-goals-p nil - "Whether the prover supports nested proofs or not. -Proof General will try to do something sensible if it does." + "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 +steps." :type 'boolean :group 'proof-script) diff --git a/generic/proof-script.el b/generic/proof-script.el index 3bd03042..30692c92 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1234,7 +1234,7 @@ the ACS is marked in the current buffer. If CMD does not match any, (let ((gspan span) ; putative goal span (savestart (span-start span)) (saveend (span-end span)) - lev goalend nam next ncmd) + lev nestedundos goalend nam next ncmd) ;; Try to set the name of the theorem from the save ;; (message "%s" cmd) 3.4: remove this message. @@ -1252,7 +1252,10 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; along the way: they will be amalgamated into a single ;; goal-save region, which corresponds to the prover ;; discarding the proof history. + ;; Provers without flat history yet nested proofs (i.e. Coq) + ;; need to keep a record of the undo count for nested goalsaves. (setq lev 1) + (setq nestedundos 0) (while (and gspan (> lev 0)) (setq next (prev-span gspan 'type)) (delete-span gspan) @@ -1261,9 +1264,13 @@ the ACS is marked in the current buffer. If CMD does not match any, (progn (setq cmd (span-property gspan 'cmd)) (cond - ;; Ignore comments, any nested goalsaves - ((eq (span-property gspan 'type) 'comment)) - ((eq (span-property gspan 'type) 'goalsave)) + ;; Ignore comments [may have null cmd setting] + ((eq (span-property gspan 'type) 'comment)) + ;; Nested goal saves: add in any nestedcmds + ((eq (span-property gspan 'type) 'goalsave) + (setq nestedundos + (+ nestedundos 1 + (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 @@ -1272,7 +1279,13 @@ the ACS is marked in the current buffer. If CMD does not match any, (incf lev)) ;; Decrement depth when a goal is hit ((funcall proof-goal-command-p cmd) - (decf lev)))))) + (decf lev)) + ;; Remainder cases: see if command matches something we + ;; should count for a global undo + ((and proof-nested-undo-regexp + (proof-string-match proof-nested-undo-regexp cmd)) + (incf nestedundos)) + )))) (if (not gspan) ;; No goal span found! Issue a warning and do nothing more. @@ -1306,6 +1319,7 @@ the ACS is marked in the current buffer. If CMD does not match any, (set-span-property gspan 'type 'goalsave) (set-span-property gspan 'idiom 'proof);; links to nested proof element (set-span-property gspan 'name nam) + (set-span-property gspan 'nestedundos nestedundos) (pg-set-span-helphighlights gspan) ;; Make a nested span which contains the purported body of the |