diff options
Diffstat (limited to 'pygments/lexers/theorem.py')
| -rw-r--r-- | pygments/lexers/theorem.py | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py index e4ed7539..d599c3f0 100644 --- a/pygments/lexers/theorem.py +++ b/pygments/lexers/theorem.py @@ -39,15 +39,16 @@ class CoqLexer(RegexLexer): 'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope', 'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Example', 'Let', 'Ltac', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', - 'Arguments', 'Types', 'Set', 'Unset', 'Contextual', 'Strict', 'Prenex', + 'Arguments', 'Types', 'Unset', 'Contextual', 'Strict', 'Prenex', 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', 'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact', 'Remark', 'Corollary', 'Proposition', 'Property', 'Goal', 'Proof', 'Restart', 'Save', 'Qed', 'Defined', 'Abort', 'Admitted', - 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', + 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Compute', 'Eval', 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', 'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing', - 'Universe', 'Polymorphic', 'Monomorphic', 'Context' + 'Universe', 'Polymorphic', 'Monomorphic', 'Context', 'Scheme', 'From', + 'Undo', 'Fail', 'Function', ) keywords2 = ( # Gallina @@ -57,7 +58,7 @@ class CoqLexer(RegexLexer): ) keywords3 = ( # Sorts - 'Type', 'Prop', 'SProp', + 'Type', 'Prop', 'SProp', 'Set', ) keywords4 = ( # Tactics @@ -78,7 +79,7 @@ class CoqLexer(RegexLexer): 'by', 'now', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega', 'lia', 'nia', 'lra', 'nra', 'psatz', 'assumption', 'solve', 'contradiction', 'discriminate', - 'congruence', + 'congruence', 'admit' ) keywords6 = ( # Control @@ -109,6 +110,10 @@ class CoqLexer(RegexLexer): (r'\s+', Text), (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), (r'\(\*', Comment, 'comment'), + (r'\b(?:[^\W\d][\w\']*\.)+[^\W\d][\w\']*\b', Name), + (r'\bEquations\b\??', Keyword.Namespace), + # Very weak heuristic to distinguish the Set vernacular from the Set sort + (r'\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace), (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), |