michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-syntax): add syntax-highlight for unfold-c hint attribute

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-06 12:57:11 -08:00
parent bc95f09828
commit 979d6494e9
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/emacs/lean-syntax.el
View file

@ -121,6 +121,7 @@
"\[decls\]" "\[strict\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]")) "\[decls\]" "\[strict\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
. 'font-lock-doc-face) . 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . 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)
;; tactics ;; tactics
("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face)) ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
(,(rx (not (any "\.")) word-start (,(rx (not (any "\.")) word-start