diff options
| -rw-r--r-- | coq/coq-syntax.el | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index bd6dce18..6bdf364b 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -911,7 +911,7 @@ Used by `coq-goal-command-p'" (defun coq-first-abstr-regexp (paren end) (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) -(defvar coq-font-lock-terms +(defvar coq-font-lock-terms-1 (list ;; lambda binders (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) @@ -926,6 +926,17 @@ Used by `coq-goal-command-p'" ) "*Font-lock table for Coq terms.") + (defcustom coq-variable-highlight-enable t + "If non-nil, tries to highlight variables of functions and theorems with + font-lock-variable-name-face" + :type 'boolean + :group 'coq) + + + (defvar coq-font-lock-terms + (if coq-variable-highlight-enable coq-font-lock-terms-1 'nil)) + + ;; According to Coq, "Definition" is both a declaration and a goal. ;; It is understood here as being a goal. This is important for ;; recognizing global identifiers, see coq-global-p. @@ -948,10 +959,13 @@ Used by `coq-goal-command-p'" (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) -(defconst coq-decl-with-hole-regexp +(defconst coq-decl-with-hole-regexp-1 (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) +(defconst coq-decl-with-hole-regexp + (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) + (defconst coq-defn-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) "\\)\\s-+\\(" coq-id "\\)")) |