From 47134c291006af068e34d4cb02b3774e33315ef9 Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Fri, 1 Feb 2008 16:58:33 +0000
Subject: coq:cutomizable bound variable highlight (finally working)

---
 coq/coq-syntax.el | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index d2cef08f..7715cbff 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -912,7 +912,14 @@ Used by `coq-goal-command-p'"
 (defun coq-first-abstr-regexp (paren end)
   (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) 
 
+(defcustom coq-variable-highlight-enable t
+  "Activates partial bound variable highlighting"
+  :type 'boolean
+  :group 'coq)
+
+
 (defvar coq-font-lock-terms
+  (if coq-variable-highlight-enable
   (list
    ;; lambda binders
    (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face)
@@ -924,7 +931,7 @@ Used by `coq-goal-command-p'"
                                         ;               (list 0 font-lock-variable-name-face)))
    ;; parenthesized binders
    (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
-   )
+   ))
   "*Font-lock table for Coq terms.")
 
 
@@ -975,9 +982,9 @@ Used by `coq-goal-command-p'"
 ;;  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)"))
 ;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>"
 (defvar coq-font-lock-keywords-1
-  (append
-   coq-font-lock-terms
-   (list
+   (append
+    coq-font-lock-terms
+    (list
     (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face)
     (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
     (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face)
@@ -991,8 +998,9 @@ Used by `coq-goal-command-p'"
           (list 2 'font-lock-keyword-face t)
           (list 1 'font-lock-function-name-face t))
 
-    (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
-    (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)
+    (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face))
+    (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)))
+    (list
     (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
     (list coq-with-with-hole-regexp 2 'font-lock-function-name-face)
     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
-- 
cgit v1.2.3