Intermediate changes

1 files changed, 38 insertions, 19 deletions

diff --git a/contrib/python/Pygments/py3/pygments/lexers/theorem.py b/contrib/python/Pygments/py3/pygments/lexers/theorem.py
index abf09ae171..79f0606c02 100644
--- a/contrib/python/Pygments/py3/pygments/lexers/theorem.py
+++ b/contrib/python/Pygments/py3/pygments/lexers/theorem.py
@@ -6,16 +6,15 @@
 
     See also :mod:`pygments.lexers.lean`
 
-    :copyright: Copyright 2006-2023 by the Pygments team, see AUTHORS.
+    :copyright: Copyright 2006-2024 by the Pygments team, see AUTHORS.
     :license: BSD, see LICENSE for details.
 """
 
-import re
-
-from pygments.lexer import RegexLexer, default, words, include
+from pygments.lexer import RegexLexer, bygroups, default, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
     Number, Punctuation, Generic, Whitespace
-from pygments.lexers.lean import LeanLexer
+# compatibility import
+from pygments.lexers.lean import LeanLexer # noqa: F401
 
 __all__ = ['CoqLexer', 'IsabelleLexer']
 
@@ -23,8 +22,6 @@ __all__ = ['CoqLexer', 'IsabelleLexer']
 class CoqLexer(RegexLexer):
     """
     For the Coq theorem prover.
-
-    .. versionadded:: 1.5
     """
 
     name = 'Coq'
@@ -32,17 +29,18 @@ class CoqLexer(RegexLexer):
     aliases = ['coq']
     filenames = ['*.v']
     mimetypes = ['text/x-coq']
+    version_added = '1.5'
 
     flags = 0 # no re.MULTILINE
 
     keywords1 = (
         # Vernacular commands
-        'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable',
+        'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Include', 'Variable',
         'Variables', 'Parameter', 'Parameters', 'Axiom', 'Axioms', 'Hypothesis',
         'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope',
-        'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Example', 'Let',
-        'Ltac', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit',
-        'Arguments', 'Types', 'Unset', 'Contextual', 'Strict', 'Prenex',
+        'Open', 'Close', 'Bind', 'Declare', 'Delimit', 'Definition', 'Example', 'Let',
+        'Ltac', 'Ltac2', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit',
+        'Arguments', 'Types', 'Contextual', 'Strict', 'Prenex',
         'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure',
         'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact',
         'Remark', 'Corollary', 'Proposition', 'Property', 'Goal',
@@ -51,7 +49,8 @@ class CoqLexer(RegexLexer):
         'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside',
         'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing',
         'Universe', 'Polymorphic', 'Monomorphic', 'Context', 'Scheme', 'From',
-        'Undo', 'Fail', 'Function',
+        'Undo', 'Fail', 'Function', 'Program', 'Elpi', 'Extract', 'Opaque',
+        'Transparent', 'Unshelve', 'Next Obligation',
     )
     keywords2 = (
         # Gallina
@@ -99,7 +98,7 @@ class CoqLexer(RegexLexer):
         '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.',
         '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-',
         '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>',
-        r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>',
+        r'\[\|', ']', '_', '`', r'\{', r'\{<', r'lp:\{\{', r'\|', r'\|]', r'\}', '~', '=>',
         r'/\\', r'\\/', r'\{\|', r'\|\}',
         # 'Π', 'Σ', # Not defined in the standard library
         'λ', '¬', '∧', '∨', '∀', '∃', '→', '↔', '≠', '≤', '≥',
@@ -115,8 +114,10 @@ class CoqLexer(RegexLexer):
             (r'\(\*', Comment, 'comment'),
             (r'\b(?:[^\W\d][\w\']*\.)+[^\W\d][\w\']*\b', Name),
             (r'\bEquations\b\??', Keyword.Namespace),
+            (r'\b(Elpi)(\s+)(Program|Query|Accumulate|Command|Typecheck|Db|Export|Tactic)?\b', bygroups(Keyword.Namespace,Text,Keyword.Namespace)),
             # Very weak heuristic to distinguish the Set vernacular from the Set sort
-            (r'\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace),
+            (r'\bUnset\b|\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace, 'set-options'),
+            (r'\b(?:String|Number)\s+Notation', Keyword.Namespace, 'sn-notation'),
             (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),
@@ -125,8 +126,8 @@ class CoqLexer(RegexLexer):
             (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved),
             # (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'),
             (r'\b([A-Z][\w\']*)', Name),
-            (r'(%s)' % '|'.join(keyopts[::-1]), Operator),
-            (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator),
+            (r'({})'.format('|'.join(keyopts[::-1])), Operator),
+            (rf'({infix_syms}|{prefix_syms})?{operators}', Operator),
 
             (r"[^\W\d][\w']*", Name),
 
@@ -146,8 +147,27 @@ class CoqLexer(RegexLexer):
             (r'[~?][a-z][\w\']*:', Name),
             (r'\S', Name.Builtin.Pseudo),
         ],
+        'set-options': [
+            (r'\s+', Text),
+            (r'[A-Z]\w*', Keyword.Namespace),
+            (r'"', String.Double, 'string'),
+            (r'\d+', Number.Integer),
+            (r'\.', Punctuation, '#pop'),
+        ],
+        'sn-notation': [
+            (r'\s+', Text),
+            # Extra keywords to highlight only in this scope
+            (r'\b(?:via|mapping|abstract|warning|after)\b', Keyword),
+            (r'=>|[()\[\]:,]', Operator),
+            (r'\b[^\W\d][\w\']*(?:\.[^\W\d][\w\']*)*\b', Name),
+            (r'\d[\d_]*', Number.Integer),
+            (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex),
+            (r'\(\*', Comment, 'comment'),
+            (r'\.', Punctuation, '#pop'),
+        ],
         'comment': [
-            (r'[^(*)]+', Comment),
+            # Consume comments like ***** as one token
+            (r'([^(*)]+|\*+(?!\)))+', Comment),
             (r'\(\*', Comment, '#push'),
             (r'\*\)', Comment, '#pop'),
             (r'[(*)]', Comment),
@@ -175,8 +195,6 @@ class CoqLexer(RegexLexer):
 class IsabelleLexer(RegexLexer):
     """
     For the Isabelle proof assistant.
-
-    .. versionadded:: 2.0
     """
 
     name = 'Isabelle'
@@ -184,6 +202,7 @@ class IsabelleLexer(RegexLexer):
     aliases = ['isabelle']
     filenames = ['*.thy']
     mimetypes = ['text/x-isabelle']
+    version_added = '2.0'
 
     keyword_minor = (
         'and', 'assumes', 'attach', 'avoids', 'binder', 'checking',