diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-03 07:18:56 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-03 07:18:56 +0000 |
| commit | 904953a4df7fc2598a46fb59f2737f411a1469d0 (patch) | |
| tree | 1e4b1d5eba8c2ffda691f98fbe5a4057e9049840 /coq/coq-syntax.el | |
| parent | c9bfe11b0664bd6478f4ae75b10004b5d20a0386 (diff) | |
First fix of bug introduced by the last font-lock fix. Not finished.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e8ec3c12..d6eef807 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -17,7 +17,7 @@ (dolist (regexp args) (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:") regexp "\\)"))) - (concat "\\_<\\(?:"res"\\)\\_>"))) + res)) (eval-when-compile (require 'span) @@ -835,6 +835,8 @@ Used by `coq-goal-command-p'" (defvar coq-tactics (append coq-state-changing-tactics coq-state-preserving-tactics)) +(defvar coq-tactics-regexp (coq-build-opt-regexp-from-db coq-tactics-db)) + (defvar coq-retractable-instruct (append coq-state-changing-tactics coq-keywords-state-changing-commands)) @@ -969,7 +971,7 @@ Group number 1 matches the name of the library which is required.") (cons (proof-regexp-alt-list coq-solve-cheat-tactics) 'coq-cheat-face) (cons (proof-regexp-alt-list coq-keywords) 'font-lock-keyword-face) (cons (proof-regexp-alt-list coq-reserved) 'font-lock-type-face) - (cons (proof-regexp-alt-list coq-tactics ) 'proof-tactics-name-face) + (cons coq-tactics-regexp 'proof-tactics-name-face) (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face) (cons (proof-regexp-alt-list (list "Set" "Type" "Prop")) 'font-lock-type-face) (cons "============================" 'font-lock-keyword-face) |