From 101e9966fdfcfc0c5a952b14bd27252884e6ccde Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Nov 2014 18:32:18 -0800 Subject: [PATCH] fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names --- src/emacs/lean-syntax.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 83a358c24..0f3287f33 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -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")))))