coq: Add some common keywords and improve recognition of Set and qualified identifiers (#2158)

. is not an operator in Coq: in this specific usage, it is only meant to build a qualified name, so this rule really corresponds to a proper lexical rule in Coq

Unlike most languages, Coq has a large set of special words that are not reserved: they may still be used as identifiers. For example Prop is a special word, which currently gets highlighted as such in Equations.Prop.Equations, but it should be recognized as a regular name there. Because of how flexible the syntax of Coq is, it's not straightforward to disambiguate things with just a bunch of regexes, so we have to rely on heuristics. Skipping qualified names from being recognized as keywords is an easy win.

1 files changed, 10 insertions, 5 deletions

diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py
index e4ed7539..d599c3f0 100644
--- a/pygments/lexers/theorem.py
+++ b/pygments/lexers/theorem.py
@@ -39,15 +39,16 @@ class CoqLexer(RegexLexer):
         'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope',
         'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Example', 'Let',
         'Ltac', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit',
-        'Arguments', 'Types', 'Set', 'Unset', 'Contextual', 'Strict', 'Prenex',
+        'Arguments', 'Types', 'Unset', 'Contextual', 'Strict', 'Prenex',
         'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure',
         'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact',
         'Remark', 'Corollary', 'Proposition', 'Property', 'Goal',
         'Proof', 'Restart', 'Save', 'Qed', 'Defined', 'Abort', 'Admitted',
-        'Hint', 'Resolve', 'Rewrite', 'View', 'Search',
+        'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Compute', 'Eval',
         'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside',
         'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing',
-        'Universe', 'Polymorphic', 'Monomorphic', 'Context'
+        'Universe', 'Polymorphic', 'Monomorphic', 'Context', 'Scheme', 'From',
+        'Undo', 'Fail', 'Function',
     )
     keywords2 = (
         # Gallina
@@ -57,7 +58,7 @@ class CoqLexer(RegexLexer):
     )
     keywords3 = (
         # Sorts
-        'Type', 'Prop', 'SProp',
+        'Type', 'Prop', 'SProp', 'Set',
     )
     keywords4 = (
         # Tactics
@@ -78,7 +79,7 @@ class CoqLexer(RegexLexer):
         'by', 'now', 'done', 'exact', 'reflexivity',
         'tauto', 'romega', 'omega', 'lia', 'nia', 'lra', 'nra', 'psatz',
         'assumption', 'solve', 'contradiction', 'discriminate',
-        'congruence',
+        'congruence', 'admit'
     )
     keywords6 = (
         # Control
@@ -109,6 +110,10 @@ class CoqLexer(RegexLexer):
             (r'\s+', Text),
             (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo),
             (r'\(\*', Comment, 'comment'),
+            (r'\b(?:[^\W\d][\w\']*\.)+[^\W\d][\w\']*\b', Name),
+            (r'\bEquations\b\??', Keyword.Namespace),
+            # Very weak heuristic to distinguish the Set vernacular from the Set sort
+            (r'\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace),
             (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),