From 63eafaae9a2b8a6e836c753dc2b505c8a47615ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Nov 2014 14:33:28 -0800 Subject: [PATCH] feat(emacs): add syntax-highlight for clear and revert tactics --- src/emacs/lean-syntax.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 4463a052c9..f0ebb2b5b4 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -122,7 +122,8 @@ ;; tactics (,(rx (not (any "\.")) word-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros" - "generalize" "generalizes" "back" "beta" "done" "exact" "repeat" "whnf" "rotate" "rotate_left" "rotate_right") + "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" + "whnf" "rotate" "rotate_left" "rotate_right") word-end) . 'font-lock-constant-face) ;; Types