max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(emacs/lean-syntax): tactic language is not a separate language anymore

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-10 14:39:59 -07:00
parent b0b008d0bd
commit a2b491e730
1 changed files with 1 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -51,29 +51,13 @@
"reducible" "irreducible" "semireducible" "wf"
"whnf" "multiple_instances" "none" "decl" "declaration"
"relation" "symm" "subst" "refl" "trans" "simp" "congr"
"backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"
"backward" "forward" "no_pattern" "begin_end" "abbreviation"
"reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder" "unify" "defeq"
"localrefinfo" "recursor"))
"lean modifiers")
(defconst lean-modifiers-regexp
(regexp-opt lean-modifiers))
(defconst lean-tactics
'("\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
"apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
"generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
"refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
"xrewrite" "krewrite" "blast" "rec_simp" "rec_inst_simp"
"inst_simp" "simp" "simp_nohyps" "simp_topdown" "esimp" "unfold" "change" "check_expr" "contradiction"
"exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
"symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
"substvars" "now" "with_options" "with_attributes" "with_attrs" "note" "replace")
"lean tactics")
(defconst lean-tactics-regexp
(eval `(rx word-start (or ,@lean-tactics) word-end)))
(defconst lean-warnings '("sorry" "exit") "lean warnings")
(defconst lean-warnings-regexp
(eval `(rx word-start (or ,@lean-warnings) word-end)))
@ -185,9 +169,6 @@
(2 'font-lock-function-name-face))
;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; tactics
("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
(,lean-tactics-regexp . 'font-lock-constant-face)
;; warnings
(,lean-warnings-regexp . 'font-lock-warning-face)
)))