diff options
| -rw-r--r-- | coq/coq-syntax.el | 23 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
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" @@ -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 ;; |