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

fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 18:32:18 -08:00
parent 186d910d0b
commit 101e9966fd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -105,7 +105,7 @@
(,(rx (or "λ" "→" "∃" "∀" ":=")) . 'font-lock-constant-face )
;; universe/inductive/theorem... "names"
(,(rx word-start
(group (or "inductive" "theorem" "example" "axiom" "lemma" "hypothesis" "definition" "constant"))
(group (or "inductive" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant"))
word-end
(zero-or-more (or whitespace "(" "{" "["))
(group (zero-or-more (not (any " \t\n\r")))))