Test for find-and-forget using Back always instead of Reset.

1 files changed, 43 insertions, 42 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 4b815d67..a3e5507b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -223,60 +223,61 @@
       (setq str (span-property span 'cmd))
       (cond
        ((eq (span-property span 'type) 'comment))
-       ((eq (span-property span 'type) 'goalsave)
 
+       ((eq (span-property span 'type) 'goalsave)
 	;; Note da 6.10.99: in Lego and Isabelle, it's trivial to forget an
 	;; unnamed theorem.  Coq really does use the identifier
-   ;; "Unnamed_thm", though!  So we don't need this test:
-   ;;(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
+	;; "Unnamed_thm", though!  So we don't need this test:
+	;;(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
 
-		  (setq ans (format coq-forget-id-command (span-property span 'name)))
-		  (if (span-property span 'nestedundos)
-				(setq nbacks (+ nbacks (span-property span 'nestedundos)))))
+	;; da: test 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)))))
 
        ((proof-string-match 
-			(concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" 
-					  proof-id 
-					  ;; Section .. End Section should be atomic!
-					  "\\)\\s-*[\\[,:.]") str)
-		  (setq ans (format coq-forget-id-command (match-string 2 str))))
+	 (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" 
+		 proof-id 
+		 ;; Section .. End Section should be atomic!
+		 "\\)\\s-*[\\[,:.]") str)
+	(setq ans (format coq-forget-id-command (match-string 2 str))))
 
        ;; If it's not a goal but it contains "Definition" then it's a
        ;; declaration
        ((and (not (coq-goal-command-p str))
-				 (proof-string-match
-				  (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str))
-		  (setq ans (format coq-forget-id-command (match-string 2 str))))
-
-		 ; Pierre: added may 29 2002
-		 ; REM:
-		 ; It is impossible to guess if a user defined command is
-		 ; backable.  This negative test bets on the fact that user
-		 ; defined commands are probably backable, which is not sure at
-		 ; all. Betting on the opposite is also wrong. I made the 
-		 ; user definable elisp variables coq-user... to avoid this
-		 ; problem anyway.
-		 ((and 
-			(not (coq-goal-command-p str)) ;; unsaved goals
-			;; now we should match all things that do not deal with Back
-			(not (proof-string-match 
-					(concat "\\`\\(" coq-tactics-regexp "\\)")
-				  str))
-			(not (proof-string-match 
-					(concat "\\`\\(" 
-							  coq-non-backable-commands-regexp
-							  "\\)")
-					str)))
-			(setq nbacks (+ nbacks 1)))
-		 )
+	     (proof-string-match
+	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str))
+	(setq ans (format coq-forget-id-command (match-string 2 str))))
+
+       ;; Pierre: added may 29 2002 
+       ;; REM: It is impossible to guess if a user defined command is
+       ;; backable.  This negative test bets on the fact that user
+       ;; defined commands are probably backable, which is not sure at
+       ;; all. Betting on the opposite is also wrong. I made the user
+       ;; definable elisp variables coq-user... to avoid this problem
+       ;; anyway.
+       ((and 
+	 (not (coq-goal-command-p str)) ;; unsaved goals
+	 ;; now we should match all things that do not deal with Back
+	 (not (proof-string-match 
+	       (concat "\\`\\(" coq-tactics-regexp "\\)")
+	       str))
+	 (not (proof-string-match 
+	       (concat "\\`\\(" 
+		       coq-non-backable-commands-regexp
+		       "\\)")
+	       str)))
+	(setq nbacks (+ nbacks 1))))
 
       (setq span (next-span span 'type)))
-
-	 (if (= nbacks 0) () 
-		(setq answers (cons (concat " Back " (int-to-string nbacks) ". ") nil)))
-	 (if ans (setq answers (cons ans answers)))
-	 (if (null answers) proof-no-command (apply 'concat answers))
-  ))
+    
+    (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))
+    ))