Mercurial Repositories > eric / file comparison
comparison: ThirdParty/Pygments/pygments/lexers/theorem.py
ThirdParty/Pygments/pygments/lexers/theorem.py
- changeset 5713
- 6762afd9f963
- parent 4697
- c2e9bf425554
equal
deleted
inserted
replaced
| 5712:f0d08bdeacf4 | 5713:6762afd9f963 |
|---|---|
| 3 pygments.lexers.theorem | 3 pygments.lexers.theorem |
| 4 ~~~~~~~~~~~~~~~~~~~~~~~ | 4 ~~~~~~~~~~~~~~~~~~~~~~~ |
| 5 | 5 |
| 6 Lexers for theorem-proving languages. | 6 Lexers for theorem-proving languages. |
| 7 | 7 |
| 8 :copyright: Copyright 2006-2015 by the Pygments team, see AUTHORS. | 8 :copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS. |
| 9 :license: BSD, see LICENSE for details. | 9 :license: BSD, see LICENSE for details. |
| 10 """ | 10 """ |
| 11 | 11 |
| 12 import re | 12 import re |
| 13 | 13 |
| 388 filenames = ['*.lean'] | 388 filenames = ['*.lean'] |
| 389 mimetypes = ['text/x-lean'] | 389 mimetypes = ['text/x-lean'] |
| 390 | 390 |
| 391 flags = re.MULTILINE | re.UNICODE | 391 flags = re.MULTILINE | re.UNICODE |
| 392 | 392 |
| 393 keywords1 = ('import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', 'renaming', | 393 keywords1 = ( |
| 394 'inline', 'hiding', 'exposing', 'parameter', 'parameters', 'conjecture', | 394 'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', |
| 395 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', 'print', 'theorem', | 395 'renaming', 'inline', 'hiding', 'exposing', 'parameter', 'parameters', |
| 396 'axiom', 'inductive', 'structure', 'universe', 'alias', 'help', | 396 'conjecture', 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', |
| 397 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', 'calc_subst', 'calc_refl', | 397 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias', |
| 398 'infix', 'infixl', 'infixr', 'notation', 'eval', 'check', 'exit', 'coercion', 'end', | 398 'help', 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', |
| 399 'private', 'using', 'namespace', 'including', 'instance', 'section', 'context', | 399 'calc_subst', 'calc_refl', 'infix', 'infixl', 'infixr', 'notation', 'eval', |
| 400 'protected', 'expose', 'export', 'set_option', 'add_rewrite', 'extends', | 400 'check', 'exit', 'coercion', 'end', 'private', 'using', 'namespace', |
| 401 'open', 'example', 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible' | 401 'including', 'instance', 'section', 'context', 'protected', 'expose', |
| 402 'export', 'set_option', 'add_rewrite', 'extends', 'open', 'example', | |
| 403 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible', | |
| 402 ) | 404 ) |
| 403 | 405 |
| 404 keywords2 = ( | 406 keywords2 = ( |
| 405 'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', 'take', | 407 'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', |
| 406 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', 'proof', 'qed', 'calc', 'match' | 408 'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', |
| 409 'proof', 'qed', 'calc', 'match', | |
| 407 ) | 410 ) |
| 408 | 411 |
| 409 keywords3 = ( | 412 keywords3 = ( |
| 410 # Sorts | 413 # Sorts |
| 411 'Type', 'Prop', | 414 'Type', 'Prop', |
| 412 ) | 415 ) |
| 413 | 416 |
| 414 operators = ( | 417 operators = ( |
| 415 '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!', '`', | 418 u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`', |
| 416 '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<', | 419 u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<', |
| 417 '<-', '=', '==', '>', '_', '`', '|', '||', '~', '=>', '<=', '>=', | 420 u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=', |
| 418 '/\\', '\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', | 421 u'/\\', u'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', |
| 419 u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', u'⌟', u'≡', | 422 u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', |
| 420 u'⟨', u'⟩' | 423 u'⌟', u'≡', u'⟨', u'⟩', |
| 421 ) | 424 ) |
| 422 | 425 |
| 423 punctuation = ('(', ')', ':', '{', '}', '[', ']', u'⦃', u'⦄', ':=', ',') | 426 punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'⦃', u'⦄', |
| 427 u':=', u',') | |
| 424 | 428 |
| 425 tokens = { | 429 tokens = { |
| 426 'root': [ | 430 'root': [ |
| 427 (r'\s+', Text), | 431 (r'\s+', Text), |
| 428 (r'/-', Comment, 'comment'), | 432 (r'/-', Comment, 'comment'), |
