diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-04-13 13:06:40 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-04-13 13:06:40 +0000 |
| commit | 6de817881dd92175165b47c672e4ab7d9fb3e4c2 (patch) | |
| tree | a6d8d09ef540a21967fe8def733f4dfc7afb4973 /coq/coq-syntax.el | |
| parent | 53ab650ed0a357bb5a70a333863c25d0b924a53e (diff) | |
Debugging font-lock for ∀, ∃, and λ.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5cb48f28..c3ef6137 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -887,8 +887,9 @@ It is used: "is" "nosimpl" "of")) "Reserved keywords of Coq.") -(defvar coq-reserved-regexp - (concat "\\<with\\s-+signature\\>\\|" +;; FIXME: ∀ and ∃ should be followed by a space in coq syntax. +(defvar coq-reserved-regexp + (concat "\\<with\\s-+signature\\>\\|\\_<∀\\_>\\|\\_<∃\\_>\\|\\_<λ\\_>\\|" (proof-ids-to-regexp coq-reserved) )) (defvar coq-state-changing-tactics @@ -965,17 +966,19 @@ It is used: :type 'boolean :group 'coq) -(defconst coq-lambda-regexp "\\<\\(?:fun\\|λ\\)\\>") +(defconst coq-lambda-regexp "\\(?:\\<fun\\>\\|\\_<λ\\_>\\)") -(defconst coq-forall-regexp "\\(?:\\<forall\\>\\|∀\\)") +(defconst coq-forall-regexp "\\(?:\\<forall\\>\\|\\_<∀\\_>\\)") +(defconst coq-exists-regexp "\\(?:\\<exists\\>\\|\\_<∃\\_>\\)") (defvar coq-font-lock-terms (if coq-variable-highlight-enable (list ;; lambda binders - (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\|,\\)") 1 'font-lock-variable-name-face) ;; forall binder (list (coq-first-abstr-regexp coq-forall-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp coq-exists-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) ; (list "\\<forall\\>" ; (list 0 font-lock-type-face) ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil @@ -1109,6 +1112,9 @@ It is used: (modify-syntax-entry ?\& ".") (modify-syntax-entry ?_ "_") (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?∀ "_") + (modify-syntax-entry ?∃ "_") + (modify-syntax-entry ?λ "_") ;; maybe a bad idea... lambda is a letter (modify-syntax-entry ?\| ".") ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug |