From f6dc6e650490f2782a4fcaabcff064ba6eb33783 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Jun 2014 13:36:35 -0700 Subject: [PATCH] feat(emacs): add new calc commands to lean emacs mode Signed-off-by: Leonardo de Moura --- src/emacs/lean-mode.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index b295a22d0f..c959dbc397 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -24,7 +24,7 @@ (define-generic-mode 'lean-mode ;; name of the mode to create '("--") ;; comments start with - '("import" "abbreviation" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords + '("import" "abbreviation" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face)