Mercurial Repositories > eric / file comparison
comparison: eric6/ThirdParty/Pygments/pygments/lexers/theorem.py
eric6/ThirdParty/Pygments/pygments/lexers/theorem.py
- changeset 7701
- 25f42e208e08
- parent 7547
- 21b0534faebc
- child 7983
- 54c5cfbb1e29
equal
deleted
inserted
replaced
| 7700:a3cf077a8db3 | 7701:25f42e208e08 |
|---|---|
| 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-2019 by the Pygments team, see AUTHORS. | 8 :copyright: Copyright 2006-2020 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 |
| 91 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', | 91 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', |
| 92 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', | 92 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', |
| 93 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', | 93 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', |
| 94 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>', | 94 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>', |
| 95 r'/\\', r'\\/', r'\{\|', r'\|\}', | 95 r'/\\', r'\\/', r'\{\|', r'\|\}', |
| 96 u'Π', u'λ', | 96 'Π', 'λ', |
| 97 ) | 97 ) |
| 98 operators = r'[!$%&*+\./:<=>?@^|~-]' | 98 operators = r'[!$%&*+\./:<=>?@^|~-]' |
| 99 prefix_syms = r'[!?~]' | 99 prefix_syms = r'[!?~]' |
| 100 infix_syms = r'[=<>@^|&+\*/$%-]' | 100 infix_syms = r'[=<>@^|&+\*/$%-]' |
| 101 | 101 |
| 386 filenames = ['*.lean'] | 386 filenames = ['*.lean'] |
| 387 mimetypes = ['text/x-lean'] | 387 mimetypes = ['text/x-lean'] |
| 388 | 388 |
| 389 flags = re.MULTILINE | re.UNICODE | 389 flags = re.MULTILINE | re.UNICODE |
| 390 | 390 |
| 391 keywords1 = ( | |
| 392 'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', | |
| 393 'renaming', 'inline', 'hiding', 'exposing', 'parameter', 'parameters', | |
| 394 'conjecture', 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', | |
| 395 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias', | |
| 396 'help', 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', | |
| 397 'calc_subst', 'calc_refl', 'infix', 'infixl', 'infixr', 'notation', 'eval', | |
| 398 'check', 'exit', 'coercion', 'end', 'private', 'using', 'namespace', | |
| 399 'including', 'instance', 'section', 'context', 'protected', 'expose', | |
| 400 'export', 'set_option', 'add_rewrite', 'extends', 'open', 'example', | |
| 401 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible', | |
| 402 ) | |
| 403 | |
| 404 keywords2 = ( | |
| 405 'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', | |
| 406 'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', | |
| 407 'proof', 'qed', 'calc', 'match', | |
| 408 ) | |
| 409 | |
| 410 keywords3 = ( | |
| 411 # Sorts | |
| 412 'Type', 'Prop', | |
| 413 ) | |
| 414 | |
| 415 operators = ( | |
| 416 u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`', | |
| 417 u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<', | |
| 418 u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=', | |
| 419 u'/\\', u'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', | |
| 420 u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', | |
| 421 u'⌟', u'≡', u'⟨', u'⟩', u'^', | |
| 422 ) | |
| 423 | |
| 424 punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'⦃', u'⦄', | |
| 425 u':=', u',') | |
| 426 | |
| 427 tokens = { | 391 tokens = { |
| 428 'root': [ | 392 'root': [ |
| 429 (r'\s+', Text), | 393 (r'\s+', Text), |
| 394 (r'/--', String.Doc, 'docstring'), | |
| 430 (r'/-', Comment, 'comment'), | 395 (r'/-', Comment, 'comment'), |
| 431 (r'--.*?$', Comment.Single), | 396 (r'--.*?$', Comment.Single), |
| 432 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), | 397 (words(( |
| 433 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), | 398 'import', 'renaming', 'hiding', |
| 434 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), | 399 'namespace', |
| 435 (words(operators), Name.Builtin.Pseudo), | 400 'local', |
| 436 (words(punctuation), Operator), | 401 'private', 'protected', 'section', |
| 437 (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]" | 402 'include', 'omit', 'section', |
| 438 u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079" | 403 'protected', 'export', |
| 439 u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name), | 404 'open', |
| 405 'attribute', | |
| 406 ), prefix=r'\b', suffix=r'\b'), Keyword.Namespace), | |
| 407 (words(( | |
| 408 'lemma', 'theorem', 'def', 'definition', 'example', | |
| 409 'axiom', 'axioms', 'constant', 'constants', | |
| 410 'universe', 'universes', | |
| 411 'inductive', 'coinductive', 'structure', 'extends', | |
| 412 'class', 'instance', | |
| 413 | |
| 414 'noncomputable theory', | |
| 415 | |
| 416 'noncomputable', 'mutual', 'meta', | |
| 417 | |
| 418 'attribute', | |
| 419 | |
| 420 'parameter', 'parameters', | |
| 421 'variable', 'variables', | |
| 422 | |
| 423 'reserve', 'precedence', | |
| 424 'postfix', 'prefix', 'notation', 'infix', 'infixl', 'infixr', | |
| 425 | |
| 426 'begin', 'by', 'end', | |
| 427 | |
| 428 'set_option', | |
| 429 'run_cmd', | |
| 430 ), prefix=r'\b', suffix=r'\b'), Keyword.Declaration), | |
| 431 (r'@\[[^\]]*\]', Keyword.Declaration), | |
| 432 (words(( | |
| 433 'forall', 'fun', 'Pi', 'from', 'have', 'show', 'assume', 'suffices', | |
| 434 'let', 'if', 'else', 'then', 'in', 'with', 'calc', 'match', | |
| 435 'do' | |
| 436 ), prefix=r'\b', suffix=r'\b'), Keyword), | |
| 437 (words(('Sort', 'Prop', 'Type'), prefix=r'\b', suffix=r'\b'), Keyword.Type), | |
| 438 (words(( | |
| 439 '#eval', '#check', '#reduce', '#exit', | |
| 440 '#print', '#help', | |
| 441 ), suffix=r'\b'), Keyword), | |
| 442 (words(( | |
| 443 '(', ')', ':', '{', '}', '[', ']', '⟨', '⟩', '‹', '›', '⦃', '⦄', ':=', ',', | |
| 444 )), Operator), | |
| 445 (r'[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]' | |
| 446 r'[.A-Za-z_\'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079' | |
| 447 r'\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*', Name), | |
| 448 (r'0x[A-Za-z0-9]+', Number.Integer), | |
| 449 (r'0b[01]+', Number.Integer), | |
| 440 (r'\d+', Number.Integer), | 450 (r'\d+', Number.Integer), |
| 441 (r'"', String.Double, 'string'), | 451 (r'"', String.Double, 'string'), |
| 442 (r'[~?][a-z][\w\']*:', Name.Variable) | 452 (r"'(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4})|.)'", String.Char), |
| 453 (r'[~?][a-z][\w\']*:', Name.Variable), | |
| 454 (r'\S', Name.Builtin.Pseudo), | |
| 443 ], | 455 ], |
| 444 'comment': [ | 456 'comment': [ |
| 445 # Multiline Comments | |
| 446 (r'[^/-]', Comment.Multiline), | 457 (r'[^/-]', Comment.Multiline), |
| 447 (r'/-', Comment.Multiline, '#push'), | 458 (r'/-', Comment.Multiline, '#push'), |
| 448 (r'-/', Comment.Multiline, '#pop'), | 459 (r'-/', Comment.Multiline, '#pop'), |
| 449 (r'[/-]', Comment.Multiline) | 460 (r'[/-]', Comment.Multiline) |
| 450 ], | 461 ], |
| 462 'docstring': [ | |
| 463 (r'[^/-]', String.Doc), | |
| 464 (r'-/', String.Doc, '#pop'), | |
| 465 (r'[/-]', String.Doc) | |
| 466 ], | |
| 451 'string': [ | 467 'string': [ |
| 452 (r'[^\\"]+', String.Double), | 468 (r'[^\\"]+', String.Double), |
| 453 (r'\\[n"\\]', String.Escape), | 469 (r"(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4}))", String.Escape), |
| 454 ('"', String.Double, '#pop'), | 470 ('"', String.Double, '#pop'), |
| 455 ], | 471 ], |
| 456 } | 472 } |
