coq: Add keywords, more syntax, and refactor lexing of comments (#2678)

pygments · Apr 3, 2024 · 234c003 · 234c003
1 parent 20cc5e5
commit 234c003
Show file tree

Hide file tree

Showing 4 changed files with 211 additions and 369 deletions.
diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
@@ -10,7 +10,7 @@
     :license: BSD, see LICENSE for details.
 """
 
-from pygments.lexer import RegexLexer, default, words
+from pygments.lexer import RegexLexer, bygroups, default, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
     Number, Punctuation, Generic, Whitespace
 # compatibility import
@@ -35,12 +35,12 @@ class CoqLexer(RegexLexer):
 
     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',
@@ -49,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
@@ -97,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
         'λ', '¬', '∧', '∨', '∀', '∃', '→', '↔', '≠', '≤', '≥',
@@ -113,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),
@@ -144,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),