Changed once again the backtrack mechanism, it corresponds to what we

agreed for some time ago. I am ok for a 3.4 now.

2 files changed, 126 insertions, 113 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 89af8ce4..7234d53b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -69,7 +69,7 @@
 
 
 
-(defcustom coq-user-backable-commands nil
+(defcustom coq-user-state-changing-commands nil
  
 "Configuration variable (default to nil). List of strings containing
 the user defined Coq commands that need to be backtracked (like
@@ -78,12 +78,12 @@ Require, Definition, etc).
 For example if MyHint and MyRequire are user defined variants of the
 Hint and Require commands, put the following line in your .emacs:
 
-(setq coq-user-backable-commands 
+(setq coq-user-state-changing-commands 
 		'(\"MyHint\" \"MyRequire\"))
 "
 )
 
-(defvar coq-user-non-backable-commands nil
+(defvar coq-user-state-preserving-commands nil
  
 "Configuration variable (default to nil). List of strings containing
 the user defined Coq commands that do not need to be backtracked (like
@@ -92,14 +92,14 @@ Print, Check, Show etc).
 For example if MyPrint and MyCheck are user defined variants of the
 Print and Check commands, put the following line in your .emacs:
 
-(setq coq-user-non-backable-commands 
+(setq coq-user-state-preserving-commands 
 		'(\"MyPrint\" \"MyCheck\"))
 "
 )
 
 ;; 
 
-(defvar coq-keywords-non-backable-commands
+(defvar coq-keywords-state-preserving-commands
   (append '(
 "(*" ;;Pierre comments must not be undone
 "Add\\s-+LoadPath"
@@ -120,7 +120,7 @@ Print and Check commands, put the following line in your .emacs:
 "Locate\\s-+Library"
 "Opaque"
 "Print"
-"Proof"; also in non-undoable-tactic
+"Proof"
 "Recursive\\-+Extraction"
 "Recursive\\-+Extraction\\-+Module"
 "Remove\\-+LoadPath"
@@ -146,14 +146,14 @@ Print and Check commands, put the following line in your .emacs:
 "Unset\\s-+Printing\\s-+Coercion[^s]"
 "Transparent"
 "Write\\s-+State")
-			 coq-user-non-backable-commands
+			 coq-user-state-preserving-commands
 			 )
   )
 
 
 
 
-(defvar coq-keywords-backable-misc-commands
+(defvar coq-keywords-state-changing-misc-commands
  '(
 "Add\\s-+Abstract\\s-+Ring"
 "Add\\s-+Abstract\\s-+Semi\\s-+Ring"
@@ -221,19 +221,19 @@ Print and Check commands, put the following line in your .emacs:
 
 
 
-(defvar coq-keywords-backable-commands
+(defvar coq-keywords-state-changing-commands
   (append
-	coq-keywords-backable-misc-commands
+	coq-keywords-state-changing-misc-commands
 	coq-keywords-decl
 	coq-keywords-defn
 	coq-keywords-goal
-	coq-user-backable-commands
+	coq-user-state-changing-commands
 	)
   )
 
 (defvar coq-keywords-commands
-  (append coq-keywords-backable-commands
-			 coq-keywords-non-backable-commands)
+  (append coq-keywords-state-changing-commands
+			 coq-keywords-state-preserving-commands)
   "All commands keyword")
 
 
@@ -241,7 +241,7 @@ Print and Check commands, put the following line in your .emacs:
  
 "Configuration variable (default to nil). List of strings containing
 the user defined Coq tactics that need to be backtracked (like almost
-all tactics, but \"Proof\").
+all tactics, but \"Idtac\" (\"Proof\" is a command actually)).
 
 For example if MyIntro and MyElim are user defined variants of the
 Intro and Elim tactics, put the following line in your .emacs:
@@ -325,6 +325,7 @@ Intro and Elim tactics, put the following line in your .emacs:
 "Reflexivity"
 "Rename"
 "Replace"
+"Resume"
 "Rewrite"
 "Right"
 "Ring"
@@ -336,6 +337,7 @@ Intro and Elim tactics, put the following line in your .emacs:
 "Split"
 "SplitAbsolu"
 "SplitRmult"
+"Suspend"
 "Symmetry"
 "Tauto"
 "Transitivity"
@@ -347,40 +349,39 @@ coq-user-undoable-tactics
 
 )
 
-(defcustom coq-user-non-undoable-tactics nil
+(defcustom coq-user-state-preserving-tactics nil
  
 "Configuration variable (default to nil). List of strings containing
 the user defined Coq tactics that do not need to be backtracked (like
-\"Proof\" (no other one to my knowledge ?)).
+\"Idtac\" (no other one to my knowledge ?)).
 
-For example if MyProof and Do_nthing are user defined variants of the
-Proof (Nop) tactic, put the following line in your .emacs:
+For example if MyIdtac and Do_nthing are user defined variants of the
+Idtac (Nop) tactic, put the following line in your .emacs:
 
-(setq coq-user-non-undoable-tactics
-		'(\"MyProof\" \"Do_nthing\"))
+(setq coq-user-state-preserving-tactics
+		'(\"MyIdtac\" \"Do_nthing\"))
 "
 )
 
-(defvar coq-non-undoable-tactics 
+(defvar coq-state-preserving-tactics 
   (append '(
-"Proof" ; also in non-backable-command
 "Idtac"
 )
-			 coq-user-non-undoable-tactics
+			 coq-user-state-preserving-tactics
 )
 )
 
 (defvar coq-tactics 
-  (append coq-undoable-tactics coq-non-undoable-tactics))
+  (append coq-undoable-tactics coq-state-preserving-tactics))
 
 
 (defvar coq-retractable-instruct
-  (append coq-undoable-tactics coq-keywords-backable-commands)
+  (append coq-undoable-tactics coq-keywords-state-changing-commands)
   )
 
 (defvar coq-non-retractable-instruct
-  (append coq-non-undoable-tactics
-			 coq-keywords-non-backable-commands)
+  (append coq-state-preserving-tactics
+			 coq-keywords-state-preserving-commands)
   )
 
 (defvar coq-keywords
@@ -392,7 +393,7 @@ Proof (Nop) tactic, put the following line in your .emacs:
   '(
     "Abstract"
     "Do"
-    "Idtac" ; also in  non-undoable-tactic
+    "Idtac" ; also in  state-preserving-tactic
     "Orelse"
     "Repeat"
     "Try")
diff --git a/coq/coq.el b/coq/coq.el
index 106b16c7..11c9fded 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -119,14 +119,14 @@
 
 (defconst coq-undoable-tactics-regexp 
   (proof-ids-to-regexp coq-undoable-tactics))
-(defconst coq-non-undoable-tactics-regexp 
-  (proof-ids-to-regexp coq-non-undoable-tactics))
+(defconst coq-state-preserving-tactics-regexp 
+  (proof-ids-to-regexp coq-state-preserving-tactics))
 (defconst coq-tactics-regexp
   (proof-ids-to-regexp coq-tactics))
-(defconst coq-backable-commands-regexp
-  (proof-ids-to-regexp coq-keywords-backable-commands))
-(defconst coq-non-backable-commands-regexp 
-  (proof-ids-to-regexp coq-keywords-non-backable-commands))
+(defconst coq-state-changing-commands-regexp
+  (proof-ids-to-regexp coq-keywords-state-changing-commands))
+(defconst coq-state-preserving-commands-regexp 
+  (proof-ids-to-regexp coq-keywords-state-preserving-commands))
 (defvar coq-retractable-instruct-regexp 
   (proof-ids-to-regexp coq-retractable-instruct))
 (defvar coq-non-retractable-instruct-regexp
@@ -185,6 +185,7 @@
   "Decide whether argument is a goal or not"
   (and (proof-string-match coq-goal-command-regexp str)
        (not (proof-string-match "Definition.*:=" str))
+		 (not (proof-string-match "Recursive Definition" str))
        ;; da: 3.4 test: do not exclude Lemma: we want goal-command-p to
        ;; succeed for nested goals too now.
        ;; (should we also exclude Definition?)
@@ -223,34 +224,34 @@ This assumes that no \"Resume\" command has been used."
        ;; [ Maybe not: Section is being treated as a _goal_ command
        ;;   now, so this test has to appear before the goalsave ]
        ((proof-string-match 
-	 (concat "Section\\s-+\\(" proof-id "\\)\\s-*") str)
-	(unless (eq (span-property span 'type) 'goalsave)
-	  ;; If we're resetting to beginning of a section from
-	  ;; inside, need to fix the nesting depth.
-	  ;; FIXME: this is not good enough: the scanning loop
-	  ;; exits immediately but Reset has implicit Aborts
-	  ;; which are not being counted here.  Really
-	  ;; we need to set the "master reset" command which
-	  ;; subsumes the others, but still count the depth.
-	  (decf proof-nesting-depth))
-	(setq ans (format coq-forget-id-command (match-string 2 str))))
+         (concat "Section\\s-+\\(" proof-id "\\)\\s-*") str)
+        (unless (eq (span-property span 'type) 'goalsave)
+          ;; If we're resetting to beginning of a section from
+          ;; inside, need to fix the nesting depth.
+          ;; FIXME: this is not good enough: the scanning loop
+          ;; exits immediately but Reset has implicit Aborts
+          ;; which are not being counted here.  Really
+          ;; we need to set the "master reset" command which
+          ;; subsumes the others, but still count the depth.
+          (decf proof-nesting-depth))
+        (setq ans (format coq-forget-id-command (match-string 2 str))))
        
        ((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)
-
-	;; da: try using just Back since "Reset" causes loss of proof
-	;; state.
-	;; (format coq-forget-id-command (span-property span 'name)))
-	(if (span-property span 'nestedundos) 
-	    (setq nbacks (+ 1 nbacks (span-property span 'nestedundos)))))
+        ;; 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)
+
+        ;; da: try using just Back since "Reset" causes loss of proof
+        ;; state.
+        ;; (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)
-	(incf naborts))
+        (incf naborts))
        
        ;; If we are already outside a proof, issue a Reset.
        ;; [ improvement would be to see if the undoing
@@ -258,53 +259,56 @@ This assumes that no \"Resume\" command has been used."
        ;;   Reset found if so: but this is tricky to co-ordinate
        ;;   with the number of Backs, perhaps? ]
        ((and 
-	 (not (coq-proof-mode-p)) ;; (eq proof-nesting-depth 0)
-	 (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))))
+         (not (coq-proof-mode-p));; (eq proof-nesting-depth 0)
+         (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))))
 
        ;; FIXME: combine with coq-keywords-decl-defn-regexp case above?
        ;; If it's not a goal but it contains "Definition" then it's a
        ;; declaration  [ da: is this not covered by above case??? ]
-       ((and (not (coq-proof-mode-p)) ;; (eq proof-nesting-depth 0)
-	     (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 
-	 ;; 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)))
-	(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.
-       ((and
-	 (eq 0 naborts)
-	 (proof-string-match 
-	       (concat "\\`\\(" 
-		       coq-undoable-tactics-regexp
-		       "\\)")
-	       str))
-	(incf nundos)))
-
+       ((and (not (coq-proof-mode-p));; (eq proof-nesting-depth 0)
+             (proof-string-match
+              (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str))
+        (setq ans (format coq-forget-id-command (match-string 2 str))))
+		 
+       ;; Outside a proof: cannot be a tactic, if unknown: do back 
+       ;; (we may decide otherwise, it is false anyhow, use elisp 
+       ;; vars instead for the perfect thing).
+       ((and (not (coq-proof-mode-p))
+             (not (proof-string-match 
+                   (concat "\\`\\(" 
+                           coq-state-preserving-commands-regexp
+                           "\\)")
+                   str)))
+        (incf nbacks))
+
+       ;; inside a proof: if known command then back or nothing (depending 
+       ;;                 on the command), 
+       ;; if known "need not undo tactic" then nothing
+       ;; otherwise : undo (unknown tactics are considered needing undo, 
+       ;;                    which is ok at 99%, use elisp vars for the 
+       ;;                    1% remaining).
+       ;; no undo if abort
+       ((coq-proof-mode-p)
+        (cond
+         ((proof-string-match 
+           (concat "\\`\\(" coq-state-changing-commands-regexp "\\)")
+           str)
+          (incf nbacks))
+         ((and (eq 0 naborts)
+               (not (proof-string-match 
+                     (concat "\\`\\(" coq-state-preserving-commands-regexp "\\)")
+                     str))
+               (not (proof-string-match 
+                     (concat "\\`\\(" coq-state-preserving-tactics-regexp "\\)")
+                     str)))
+          (incf nundos))
+         ))
+       )
       (setq span (next-span span 'type)))
     
     ;; Now adjust proof-nesting depth according to the
@@ -315,21 +319,21 @@ This assumes that no \"Resume\" command has been used."
     (setq proof-nesting-depth (- proof-nesting-depth naborts))
 
     (setq ans
-	  (concat
-	   (if (stringp ans) ans)
-	   (if (> naborts 0)
-	       ;; ugly, but blame Coq
-	       (let ((aborts "Abort. "))
-		 (while (> (decf naborts) 0)
-		   (setq aborts (concat "Abort. " aborts)))
-		 aborts))
-	   (if (> nbacks 0)
-	       (concat "Back " (int-to-string nbacks) ". "))
-	   (if (> nundos 0) 
-	       (concat "Undo " (int-to-string nundos) ". "))))
+          (concat
+           (if (stringp ans) ans)
+           (if (> naborts 0)
+               ;; ugly, but blame Coq
+               (let ((aborts "Abort. "))
+                 (while (> (decf naborts) 0)
+                   (setq aborts (concat "Abort. " aborts)))
+                 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)
+        proof-no-command;; FIXME: this is an error really (assert nil)
       ans)))
   
 
@@ -572,7 +576,7 @@ This is specific to coq-mode."
   (setq proof-save-command-regexp coq-save-command-regexp
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
 	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
-	proof-nested-undo-regexp coq-backable-commands-regexp)
+	proof-nested-undo-regexp coq-state-changing-commands-regexp)
   
   (setq	
    proof-indent-close-offset -1
@@ -787,3 +791,11 @@ This is specific to coq-mode."
 		proof-shell-inform-file-retracted-cmd nil)))
 
 (provide 'coq)
+
+
+;;;   Local Variables: ***
+;;;   tab-width:2 ***
+;;;   indent-tabs-mode:nil ***
+;;;   End: ***
+
+