diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | coq/coq-db.el | 9 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 53 |
3 files changed, 47 insertions, 20 deletions
@@ -142,8 +142,9 @@ the GIT ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Removed the Set Undo 500 at start. This is obsolete. To recover: (setq coq-user-init-cmd `("Set Undo 500.")) - - +*** Option to highlight usual symbols + Off by default, enable using: + (setq coq-symbol-highlight-enable t) **** Minibuffer interactive queries diff --git a/coq/coq-db.el b/coq/coq-db.el index 25eee637..0d9c0a6e 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -305,6 +305,11 @@ See `coq-syntax-db' for DB structure." "Face for unicode binders, by default a bold version of `font-lock-type-face'." :group 'proof-faces) +(defface coq-symbol-face + '((t :inherit default-face :bold coq-bold-unicode-binders)) + "Face for unicode binders, by default a bold version of `font-lock-type-face'." + :group 'proof-faces) + (defface coq-question-mark-face '((t :inherit font-lock-variable-name-face)) "Face for Ltac binders and evars." @@ -327,6 +332,10 @@ Required so that 'coq-cheat-face is a proper facename") "Expression that evaluates to a face. Required so that 'coq-symbol-binder-face is a proper facename") +(defconst coq-symbol-face 'coq-symbol-face + "Expression that evaluates to a face. +Required so that 'coq-symbol-binder-face is a proper facename") + (defconst coq-question-mark-face 'coq-question-mark-face) 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.") |