somme little changes to make undo work better

2 files changed, 21 insertions, 4 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 049f9f53..e4d8b984 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -20,6 +20,8 @@
 "Section"				
 "Variable[s]?"
 "Global\\s-+Variable"
+;;added tactic def here because it needs Reset to be undone correctly
+"Tactic\\s-+Definition"
 ))
 
 (defvar coq-keywords-defn
@@ -58,8 +60,14 @@
 (defvar coq-keywords-kill-goal '(
 "Abort"
 ))
+;; commands that have to be counted when undoing
+(defvar coq-keywords-undoable-commands
+  '(
+"Focus"
+))
 
-(defvar coq-keywords-commands
+
+(defvar coq-keywords-not-undoable-commands
   '(
 "Add\\s-+ML\\s-+Path"
 "AddPath"
@@ -74,7 +82,8 @@
 "End\\s-+Silent"
 "Eval"
 "Extraction"
-"Focus"
+;; moving this to coq-keywords-undoable-commands
+;;"Focus"
 "Grammar"
 "Hints\\s-+Resolve"
 "Hints\\s-+Immediate"
@@ -116,10 +125,18 @@
 "Show\\s-+Script"
 "Show"
 "Syntax"
-"Tactic\\s-+Definition"
+;;Pierre: moving this to coq-keywords-decl
+;;"Tactic\\s-+Definition"
 "Transparent"
 ))
 
+
+(defvar coq-keywords-commands
+  (append coq-keywords-not-undoable-commands  coq-keywords-undoable-commands)
+  "All commands keyword")
+
+
+
 (defvar coq-tactics
   '(
 "Absurd"
diff --git a/coq/coq.el b/coq/coq.el
index 80f5cf12..5f711f89 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -109,7 +109,7 @@
 (defconst coq-kill-goal-command "Abort.")
 (defconst coq-forget-id-command "Reset %s.")
 
-(defconst coq-undoable-commands-regexp (proof-ids-to-regexp coq-tactics))
+(defconst coq-undoable-commands-regexp (proof-ids-to-regexp (append coq-tactics coq-keywords-undoable-commands)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;