Add nestedundos setting to span, and proof-nested-undo-regexp setting

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