Mercurial Repositories > eric / file comparison
comparison: eric6/ThirdParty/Pygments/pygments/lexers/theorem.py
eric6/ThirdParty/Pygments/pygments/lexers/theorem.py
- changeset 7983
- 54c5cfbb1e29
- parent 7701
- 25f42e208e08
equal
deleted
inserted
replaced
| 7982:48d210e41c65 | 7983:54c5cfbb1e29 |
|---|---|
| 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-2020 by the Pygments team, see AUTHORS. | 8 :copyright: Copyright 2006-2021 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 |
| 27 | 27 |
| 28 name = 'Coq' | 28 name = 'Coq' |
| 29 aliases = ['coq'] | 29 aliases = ['coq'] |
| 30 filenames = ['*.v'] | 30 filenames = ['*.v'] |
| 31 mimetypes = ['text/x-coq'] | 31 mimetypes = ['text/x-coq'] |
| 32 | |
| 33 flags = re.UNICODE | |
| 32 | 34 |
| 33 keywords1 = ( | 35 keywords1 = ( |
| 34 # Vernacular commands | 36 # Vernacular commands |
| 35 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable', | 37 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable', |
| 36 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Hypothesis', | 38 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Hypothesis', |
| 121 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), | 123 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), |
| 122 (r'0[oO][0-7][0-7_]*', Number.Oct), | 124 (r'0[oO][0-7][0-7_]*', Number.Oct), |
| 123 (r'0[bB][01][01_]*', Number.Bin), | 125 (r'0[bB][01][01_]*', Number.Bin), |
| 124 (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float), | 126 (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float), |
| 125 | 127 |
| 126 (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", | 128 (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", String.Char), |
| 127 String.Char), | 129 |
| 128 (r"'.'", String.Char), | 130 (r"'.'", String.Char), |
| 129 (r"'", Keyword), # a stray quote is another syntax element | 131 (r"'", Keyword), # a stray quote is another syntax element |
| 130 | 132 |
| 131 (r'"', String.Double, 'string'), | 133 (r'"', String.Double, 'string'), |
| 132 | 134 |
| 133 (r'[~?][a-z][\w\']*:', Name), | 135 (r'[~?][a-z][\w\']*:', Name), |
| 136 (r'\S', Name.Builtin.Pseudo), | |
| 134 ], | 137 ], |
| 135 'comment': [ | 138 'comment': [ |
| 136 (r'[^(*)]+', Comment), | 139 (r'[^(*)]+', Comment), |
| 137 (r'\(\*', Comment, '#push'), | 140 (r'\(\*', Comment, '#push'), |
| 138 (r'\*\)', Comment, '#pop'), | 141 (r'\*\)', Comment, '#pop'), |
| 152 default('#pop') | 155 default('#pop') |
| 153 ], | 156 ], |
| 154 } | 157 } |
| 155 | 158 |
| 156 def analyse_text(text): | 159 def analyse_text(text): |
| 157 if text.startswith('(*'): | 160 if 'Qed' in text and 'Proof' in text: |
| 158 return True | 161 return 1 |
| 159 | 162 |
| 160 | 163 |
| 161 class IsabelleLexer(RegexLexer): | 164 class IsabelleLexer(RegexLexer): |
| 162 """ | 165 """ |
| 163 For the `Isabelle <http://isabelle.in.tum.de/>`_ proof assistant. | 166 For the `Isabelle <http://isabelle.in.tum.de/>`_ proof assistant. |
| 408 'lemma', 'theorem', 'def', 'definition', 'example', | 411 'lemma', 'theorem', 'def', 'definition', 'example', |
| 409 'axiom', 'axioms', 'constant', 'constants', | 412 'axiom', 'axioms', 'constant', 'constants', |
| 410 'universe', 'universes', | 413 'universe', 'universes', |
| 411 'inductive', 'coinductive', 'structure', 'extends', | 414 'inductive', 'coinductive', 'structure', 'extends', |
| 412 'class', 'instance', | 415 'class', 'instance', |
| 416 'abbreviation', | |
| 413 | 417 |
| 414 'noncomputable theory', | 418 'noncomputable theory', |
| 415 | 419 |
| 416 'noncomputable', 'mutual', 'meta', | 420 'noncomputable', 'mutual', 'meta', |
| 417 | 421 |
| 432 (words(( | 436 (words(( |
| 433 'forall', 'fun', 'Pi', 'from', 'have', 'show', 'assume', 'suffices', | 437 'forall', 'fun', 'Pi', 'from', 'have', 'show', 'assume', 'suffices', |
| 434 'let', 'if', 'else', 'then', 'in', 'with', 'calc', 'match', | 438 'let', 'if', 'else', 'then', 'in', 'with', 'calc', 'match', |
| 435 'do' | 439 'do' |
| 436 ), prefix=r'\b', suffix=r'\b'), Keyword), | 440 ), prefix=r'\b', suffix=r'\b'), Keyword), |
| 441 (words(('sorry', 'admit'), prefix=r'\b', suffix=r'\b'), Generic.Error), | |
| 437 (words(('Sort', 'Prop', 'Type'), prefix=r'\b', suffix=r'\b'), Keyword.Type), | 442 (words(('Sort', 'Prop', 'Type'), prefix=r'\b', suffix=r'\b'), Keyword.Type), |
| 438 (words(( | 443 (words(( |
| 439 '#eval', '#check', '#reduce', '#exit', | 444 '#eval', '#check', '#reduce', '#exit', |
| 440 '#print', '#help', | 445 '#print', '#help', |
| 441 ), suffix=r'\b'), Keyword), | 446 ), suffix=r'\b'), Keyword), |
