From 93f04f3034715b26fdd2f8d4c63d8d4108af1813 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Feb 2015 10:35:38 -0800 Subject: [PATCH] feat(emacs): update syntax highlight --- src/emacs/lean-syntax.el | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 338150f35..043e5bc5a 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -17,7 +17,7 @@ "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes" - "instances" "coercions" "raw") + "instances" "coercions" "metaclasses" "raw") "lean keywords") (defconst lean-syntax-table @@ -118,7 +118,8 @@ ;; modifiers (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]" "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" - "\[decls\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]")) + "\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" + "\[notations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]")) . 'font-lock-doc-face) (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)