From 8d50405e682fbe123cceaec1a1ba80f85bd52c5e Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 21 Dec 2015 15:54:00 -0500
Subject: [PATCH] chore(library/extras/latex/lstlean.text): update lists for
 syntax highlighting

---
 extras/latex/lstlean.tex | 49 +++++++++++++++++++++-------------------
 1 file changed, 26 insertions(+), 23 deletions(-)

diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex
index eb7873aadc..2ac9499af7 100644
--- a/extras/latex/lstlean.tex
+++ b/extras/latex/lstlean.tex
@@ -9,49 +9,52 @@ mathescape=true,
 % Comments may or not include Latex commands
 texcl=false,
 
-% keywords
+% keywords, list taken from lean-syntax.el
 morekeywords=[1]{
-import, prelude, tactic_hint, protected, private, definition, renaming,
+import, prelude, tactic_hint, protected, private, noncomputable, definition, renaming,
 hiding, exposing, parameter, parameters, begin, begin+, proof, qed, conjecture, constant, constants,
-hypothesis, lemma, corollary, variable, variables, premise, premises,
-print, theorem, example, abbreviation,
-open, as, export, axiom, axioms, inductive, with, structure, record, universe, universes,
+hypothesis, lemma, corollary, variable, variables, premise, premises, theory,
+print, theorem, proposition, example, abbreviation, abstract,
+open, as, export, override, axiom, axioms, inductive, with, structure, record, universe, universes,
 alias, help, environment, options, precedence, reserve,
 match, infix, infixl, infixr, notation, postfix, prefix,
 tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
-eval, check, coercion, end, reveal,
+eval, check, coercion, end, reveal, this, suppose,
 using, namespace, section, fields, find_decl,
-attribute, local, set_option, add_rewrite, extends, include, omit, classes,
+attribute, local, set_option, extends, include, omit, classes,
 instances, coercions, metaclasses, raw, migrate, replacing,
-calc, have, obtains, show, by, by+, in, at, let, forall, fun,
-exists, if, dif, then, else, assume, assert, take, obtain, from
+calc, have, obtains, show, suffices, by, by+, in, at, let, forall, Pi, fun,
+exists, if, dif, then, else, assume, assert, take, 
+obtain, from, aliases
 },
 
 % Sorts
 morekeywords=[2]{Type, Prop},
 
-% tactics
+% tactics, list taken from lean-syntax.el
 morekeywords=[3]{
 Cond, or_else, then, try, when, assumption, eassumption, rapply,
-apply, fapply, eapply, rename, intro, intros, all_goals, fold,
+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, esimp,
-unfold, change, check_expr, contradiction, exfalso, split, existsi, constructor, left, right,
-injection, congruence, reflexivity, symmetry, transitivity, state, induction, induction_using
+refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite, 
+xrewrite, krewrite, blast, simp, 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
 },
 
-% attributes
+% modifiers, taken from lean-syntax.el 
 % note: 'otherkeywords' is needed because these use a different symbol.
 % this command doesn't allow us to specify a number -- they are put with [1]
 otherkeywords={
-[persistent], [notation], [visible], [instance], [class], [parsing-only],
-[coercion], [unfold-f], [constructor], [reducible],
-[irreducible], [semireducible], [quasireducible], [wf],
-[whnf], [multiple-instances], [none],
-[decls], [declarations], [coercions], [classes],
-[symm], [subst], [refl], [trans], [recursor],
-[notations], [abbreviations], [begin-end-hints], [tactic-hints],
-[reduce-hints], [unfold-hints], [aliases], [eqv], [localrefinfo]
+[persistent], [notation], [visible], [instance], [trans_instance],
+[class], [parsing-only], [coercion], [unfold_full], [constructor], 
+[reducible], [irreducible], [semireducible], [quasireducible], [wf],
+[whnf], [multiple_instances], [none], [decls], [declarations], 
+[coercions], [classes], [symm], [subst], [refl], [trans], [simp], [simps], [congr], 
+[forward], [no_pattern], [notations], [abbreviations], [begin_end_hints], [tactic_hints],
+[reduce_hints], [unfold_hints], [aliases], [eqv], [intro], [intro!], [elim], 
+[localrefinfo] [recursor]
 },
 
 % Various symbols