Revised find-and-forget function, which also works for count-undos.

1 files changed, 74 insertions, 28 deletions

diff --git a/coq/coq.el b/coq/coq.el
index a3e5507b..194a572d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -113,6 +113,7 @@
 (defvar coq-shell-outline-regexp coq-goal-regexp)
 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
 
+;; 3.4: no longer use generic kill-goal-command setting
 (defconst coq-kill-goal-command "Abort.")
 (defconst coq-forget-id-command "Reset %s.")
 (defconst coq-back-n-command "Back %s. ") ; Pierre: added 
@@ -167,29 +168,50 @@
 ;;
 ;; FIXME Papageno 05/1999: must take sections in account.
 ;;
+
+;;
+;; FIXME da: combine count-undos and find-and-forget, they're
+;; the same now we deal with nested proofs.
+;;
 (defun coq-count-undos (span)
   "Count number of undos in a span, return the command needed to undo that far."
-  (let ((ct 0) str i)
+  (let ((undos 0) (backs 0) str i)
     (if (and span (prev-span span 'type)
 	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
 	     (coq-goal-command-p
 	      (span-property (prev-span span 'type) 'cmd)))
+	;; FIXME: da: is Restart really necessary/useful?  Small
+	;; efficiency gain perhaps, but this test only works in case
+	;; the previous command is exaundosly a goal.  If there are
+	;; intervening comments, Undos are issued using code below,
+	;; which still works okay I think.
 	"Restart."
       (while span
 	(setq str (span-property span 'cmd))
-	(cond ((eq (span-property span 'type) 'vanilla)
-	       (if (proof-string-match coq-undoable-tactics-regexp str)
-				  (setq ct (+ 1 ct))))
-	      ((eq (span-property span 'type) 'pbp)
-	       (cond ((proof-string-match coq-undoable-tactics-regexp str)
-		      (setq i 0)
-		      (while (< i (length str))
-			(if (= (aref str i) proof-terminal-char)
-			    (setq ct (+ 1 ct)))
-			(setq i (+ 1 i))))
-		     (t nil))))
+	(cond 
+	 ((eq (span-property span 'type) 'vanilla)
+	  (cond
+	   ((proof-string-match coq-backable-commands-regexp str)
+	    (incf backs))
+	   ((proof-string-match coq-undoable-tactics-regexp str)
+	    (incf undos))))
+	 ((span-property span 'nestedundos)
+	  (setq nbacks (+ 1 nbacks (span-property span 'nestedundos))))
+	 ((eq (span-property span 'type) 'pbp)
+	  ;; this is dead code for Coq right now, no PBP feature in PG.
+	  (cond ((proof-string-match coq-undoable-tactics-regexp str)
+		 (setq i 0)
+		 (while (< i (length str))
+		   (if (= (aref str i) proof-terminal-char)
+		       (setq undos (+ 1 undos)))
+		   (setq i (+ 1 i))))
+		(t nil))))
 	(setq span (next-span span 'type)))
-      (concat "Undo " (int-to-string ct) "."))))
+      (concat
+       (if (> undos 0) 
+	   (concat "Undo " (int-to-string undos) ". ") "")
+       (if (> backs 0)
+	   (concat "Back " (int-to-string backs) "."))))))
 
 (defconst coq-keywords-decl-defn-regexp
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
@@ -216,10 +238,15 @@
 
 ;; Pierre: May 29 2002 added a "Back n." command in order to
 ;; synchronize more accurately.
+ 
+;; DA: rewrote to combine behaviour with count-undos, to work with
+;; nested proofs.
 
 (defun coq-find-and-forget (span)
-  (let (str ans (nbacks 0) answers) 
-    (while (and span (not ans))
+  ;; NB!! Ugly use of dynamic binding here: use "end" value
+  ;; from caller as stopping value for loop velow.
+  (let (str ans (nbacks 0) (nundos 0) aborts)
+    (while (and span (< (span-start span) end) (not ans))
       (setq str (span-property span 'cmd))
       (cond
        ((eq (span-property span 'type) 'comment))
@@ -230,13 +257,19 @@
 	;; "Unnamed_thm", though!  So we don't need this test:
 	;;(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
 
-	;; da: test using just Back since "Reset" causes loss of proof
+	;; da: try using just Back since "Reset" causes loss of proof
 	;; state.
-	(setq ans t) ;; force exit
 	;; (format coq-forget-id-command (span-property span 'name)))
 	(if (span-property span 'nestedundos)
 	    (setq nbacks (+ 1 nbacks (span-property span 'nestedundos)))))
 
+       ;; Unsaved goal commands: each time we hit one of these
+       ;; we need to issue Abort to drop the proof state.
+       ((coq-goal-command-p str)
+	(setq aborts (concat coq-kill-goal-command " " aborts)))
+
+       ;; FIXME da: should we forget sections and Definitions using
+       ;; Back?
        ((proof-string-match 
 	 (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" 
 		 proof-id 
@@ -269,17 +302,27 @@
 		       coq-non-backable-commands-regexp
 		       "\\)")
 	       str)))
-	(setq nbacks (+ nbacks 1))))
+	(incf nbacks))
+
+       ;; Finally all other proof commands, which are undone with
+       ;; Undo.  But only count them if they are outermost, not
+       ;; within an aborted goal.
+       ((not aborts)
+	(incf nundos)))
 
       (setq span (next-span span 'type)))
     
-    (if (= nbacks 0) () 
-      (setq answers (cons (concat " Back " (int-to-string nbacks) ". ") nil)))
-    (if (stringp ans) (setq answers (cons ans answers)))
-    (if (null answers) proof-no-command (apply 'concat answers))
-    ))
-
-  
+    (setq ans
+	  (concat
+	   (if (stringp ans) ans)
+	   aborts
+	   (if (> nbacks 0)
+	       (concat "Back " (int-to-string nbacks) ". "))
+	   (if (> nundos 0) 
+	       (concat "Undo " (int-to-string nundos) ". "))))
+    (if (null ans) 
+	proof-no-command ;; FIXME: this is an error really (assert nil)
+      ans)))
   
 
 (defvar coq-current-goal 1
@@ -526,13 +569,16 @@ This is specific to coq-mode."
 	proof-context-command "Print All."
 	proof-goal-command "Goal %s."
 	proof-save-command "Save %s."
-	proof-find-theorems-command "Search %s."
+	proof-find-theorems-command "Search %s.")
 ;; FIXME da: Does Coq have a help or about command?
 ;;	proof-info-command "Help"
-	proof-kill-goal-command coq-kill-goal-command)
+
+;; 3.4: this is no longer used
+  (setq proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
-	proof-count-undos-fn 'coq-count-undos
+	;;proof-count-undos-fn 'coq-count-undos
+	proof-count-undos-fn     'coq-find-and-forget
 	proof-find-and-forget-fn 'coq-find-and-forget
         proof-goal-hyp-fn 'coq-goal-hyp
 	proof-state-preserving-p 'coq-state-preserving-p