Adding the option to highlight susual symbols.

This may look ugly to the majority, so I let it off by default.
I find it helpfull to have structuring symbols bold.

1 files changed, 35 insertions, 18 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 920fb439..8b09818b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1115,6 +1115,7 @@ It is used:
 (defvar coq-symbol-binders "∀\\|∃\\|λ")
 
 
+
  ;; From JF Monin:
 (defvar coq-reserved
   (append
@@ -1186,9 +1187,17 @@ It is used:
     "++>"
     "@"
     "->"
-    ".")
+    "."
+    "∧"
+    "∨"
+    "→"
+    "\\/"
+    "/\\"
+    "->")
   "Punctuation Symbols used by Coq.")
 
+(defvar coq-symbols-regexp (regexp-opt coq-symbols))
+
 ;; ----- regular expressions
 (defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
   "A regexp indicating that the Coq process has identified an error.")
@@ -1210,29 +1219,37 @@ It is used:
   :type 'boolean
   :group 'coq)
 
+(defcustom coq-symbol-highlight-enable nil
+  "Activates partial bound variable highlighting"
+  :type 'boolean
+  :group 'coq)
+
 (defconst coq-lambda-regexp "\\(?:\\_<fun\\_>\\|λ\\)")
 
 (defconst coq-forall-regexp "\\(?:\\_<forall\\_>\\|∀\\)")
 (defconst coq-exists-regexp "\\(?:\\_<exists\\_>\\|∃\\)")
 
 (defvar coq-font-lock-terms
-  (cons
-   (cons coq-symbol-binders 'coq-symbol-binder-face)
-   (if coq-variable-highlight-enable
-       (list
-        ;; lambda binders
-        (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
-        ;;               (list 0 font-lock-variable-name-face)))
-        ;; parenthesized binders
-        (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
-        (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
-        )))
+  (append   
+   (list ;; flattened by append above
+    (cons coq-symbol-binders 'coq-symbol-binder-face))
+   (when coq-symbol-highlight-enable
+     (list (cons coq-symbols-regexp 'coq-symbol-face)))
+   (when coq-variable-highlight-enable
+     (list
+      ;; lambda binders
+      (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
+      ;;               (list 0 font-lock-variable-name-face)))
+      ;; parenthesized binders
+      (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
+      (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
+      )))
   "*Font-lock table for Coq terms.")