From 9576f4a390e7493bd966e92ef87b8012b31bcb95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Jan 2021 12:14:59 -0800 Subject: [PATCH] chore: highlight `elab` --- lean4-mode/lean4-syntax.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index 12343cbc85..89dcad1819 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -19,7 +19,7 @@ "attributes" "raw" "have" "show" "suffices" "by" "in" "at" "do" "let" "for" "unless" "break" "continue" "try" "catch" "finally" "where" "rec" "mut" "forall" "fun" "exists" "if" "then" "else" "from" "init_quot" "return" - "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" + "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" "elab" "initialize" "builtin_initialize" "induction" "cases" "generalizing" "unif_hint" "deriving") "lean keywords ending with 'word' (not symbol)") (defconst lean4-keywords1-regexp