Modification of the coq-find-and-forget function, in order to use the

new "Back n." command of coq  to make the syncronization better. Seems
to work, need to test.

2 files changed, 59 insertions, 32 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 870b578b..b67da0f5 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -68,43 +68,23 @@
 "Focus"
 ))
 
-
-(defvar coq-keywords-not-undoable-commands
+(defvar coq-keywords-not-undoable-not-backable-commands
   '(
 "(*" ;;Pierre comments must not be undone
 "Add\\s-+LoadPath"
 "Add\\s-+Rec\\s-+LoadPath"
 "Add\\s-+ML\\s-+Path"
 "AddPath"
-"Begin\\s-+Silent"
 "Cd"
 "Check"
-"Class"
-"Coercion"
 "DelPath"
 "End"
 "End\\s-+Silent"
 "Eval"
 "Extraction"
-;; moving this to coq-keywords-undoable-commands
-;;"Focus"
-"Grammar"
-"Hints\\s-+Resolve"
-"Hints\\s-+Immediate"
-"Hints\\s-+Unfold"
-"HintRewrite"
-"Hint"
-"Infix"
-"Initialize"
-"Implicits";; undoable??
-"Implicit\\s-+Arguments\\s-+On"
-"Implicit\\s-+Arguments\\s-+Off"
-"Load"
-"Local\\s-+Coercion"
 "Locate\\s-+File"
 "Locate\\s-+Library"
 "Locate"
-"Opaque"
 "Print\\s-+Classes"
 "Print\\s-+Coercions"
 "Print\\s-+Graph"
@@ -117,25 +97,54 @@
 "Print"
 "Proof"
 "Pwd"
-"Require\\s-+Export"
-"Require\\s-+Import"
-"Require"
 "Reset"
 "Search"
 "SearchIsos"
 "SearchPattern"
 "SearchRewrite"
-;; da: testing moving this 
-;; "Section"
 "Show\\s-+Programs"
 "Show\\s-+Proof"
 "Show\\s-+Script"
 "Show"
+	 )
+)
+
+
+
+
+
+
+
+(defvar coq-keywords-backable-commands
+  '(
+"Begin\\s-+Silent"
+"Class"
+"Coercion"
+"Grammar"
+"Hints\\s-+Resolve"
+"Hints\\s-+Immediate"
+"Hints\\s-+Unfold"
+"HintRewrite"
+"Hint"
+"Implicits";; undoable??
+"Implicit\\s-+Arguments\\s-+On"
+"Implicit\\s-+Arguments\\s-+Off"
+"Infix"
+"Initialize" ;; What is that ??
+"Load"
+"Local\\s-+Coercion"
+"Opaque"
+"Require\\s-+Export"
+"Require\\s-+Import"
+"Require"
 "Syntax"
-;;Pierre: moving this to coq-keywords-decl
-;;"Tactic\\s-+Definition"
 "Transparent"
-))
+	 )
+)
+
+(defvar coq-keywords-not-undoable-commands
+  (append coq-keywords-backable-commands coq-keywords-not-undoable-not-backable-commands)
+)
 
 
 (defvar coq-keywords-commands
diff --git a/coq/coq.el b/coq/coq.el
index 8a71696f..d9352f58 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -115,11 +115,14 @@
 
 (defconst coq-kill-goal-command "Abort.")
 (defconst coq-forget-id-command "Reset %s.")
+(defconst coq-back-n-command "Back %s. ") ; Pierre: added 
 
 (defconst coq-undoable-commands-regexp (proof-ids-to-regexp (append coq-tactics coq-keywords-undoable-commands)))
 
 (defconst coq-not-undoable-commands-regexp (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-not-undoable-commands)))
 
+(defconst coq-backable-commands-regexp (proof-ids-to-regexp coq-keywords-backable-commands))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -200,7 +203,7 @@
 ;; TODO : add the stuff to handle the "Correctness" command
 
 (defun coq-find-and-forget (span)
-  (let (str ans)
+  (let (str ans (nbacks 0) answers) 
     (while (and span (not ans))
       (setq str (span-property span 'cmd))
       (cond
@@ -237,11 +240,26 @@
        ((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)))))
+	(setq ans (format coq-forget-id-command (match-string 2 str))))
+
+		 ; Pierre: added may 29
+		 ((proof-string-match 
+			(concat "\\`\\(" coq-backable-commands-regexp	"\\)") str)
+		  (setq nbacks (+ nbacks 1)))
+		 )
 
       (setq span (next-span span 'type)))
 
-      (or ans proof-no-command)))
+	 (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))
+  ))
+
+;  (or ans proof-no-command)
+
+  
+  
 
 (defvar coq-current-goal 1
   "Last goal that emacs looked at.")