From 6de817881dd92175165b47c672e4ab7d9fb3e4c2 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 13 Apr 2015 13:06:40 +0000
Subject: Debugging font-lock for ∀, ∃, and λ.

---
 coq/coq-syntax.el | 16 +++++++++++-----
 1 file 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
-- 
cgit v1.2.3