Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[vscode] Syntax highlighting for Coq 8.17-8.20 #872

Merged
merged 1 commit into from
Nov 15, 2024
Merged

[vscode] Syntax highlighting for Coq 8.17-8.20 #872

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

- [fleche] fix quick fixes for errors being lost due to incorrect
handling of `send_diags_extra_data` (@ejgallego, #850)
- [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)

# coq-lsp 0.2.2: To Virtual or not To Virtual
---------------------------------------------
Expand Down
135 changes: 123 additions & 12 deletions editor/code/syntaxes/coq.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
"name": "Coq",
"patterns": [
{
"match": "\\b(From|Require|Import|Export|Local|Global|Include)\\b",
"match": "\\b(From|Require|Import|Export|Local|Global|Include|Load|Dependency)\\b",
"comment": "Vernacular import keywords",
"name": "keyword.control.import.coq"
},
Expand All @@ -13,7 +13,7 @@
"name": "keyword.control.import.coq"
},
{
"match": "(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition|Goal)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"match": "\\b(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Theorem declarations",
"captures": {
"1": {
Expand All @@ -24,6 +24,18 @@
}
}
},
{
"match": "\\b(Goal)\\s+",
"comment": "Goal declaration",
"captures": {
"1": {
"name": "keyword.source.coq"
},
"2": {
"name": "entity.name.function.theorem.coq"
}
}
},
{
"match": "\\b(Parameters?|Axioms?|Conjectures?|Variables?|Hypothesis|Hypotheses)(\\s+Inline)?\\b\\s*\\(?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Assumptions",
Expand All @@ -40,7 +52,7 @@
}
},
{
"match": "\\b(Context)\\b\\s*`?\\s*(\\(|\\{)?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"match": "\\b(Context)\\b\\s*`?\\s*(\\(|\\{|\\[)?\\s*!?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Context",
"captures": {
"1": {
Expand All @@ -52,7 +64,7 @@
}
},
{
"match": "(\\b(?:Program|Local)\\s+)?\\b(Definition|Fixpoint|CoFixpoint|Function|Example|Let(?:\\s+Fixpoint|\\s+CoFixpoint)?|Instance)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"match": "(\\b(?:Program)\\s+)?\\b(Definition|Fixpoint|CoFixpoint|Function|Example|Let(?:\\s+Fixpoint|\\s+CoFixpoint)?|Instance|Primitive|SubClass)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Definitions",
"captures": {
"1": {
Expand All @@ -67,7 +79,7 @@
}
},
{
"match": "\\b((Show\\s+)?Obligation\\s+Tactic|Obligations\\s+of|Obligation|Next\\s+Obligation(\\s+of)?|Solve\\s+Obligations(\\s+of)?|Solve\\s+All\\s+Obligations|Admit\\s+Obligations(\\s+of)?|Instance)\\b",
"match": "\\b(Obligation\\s+Tactic|Obligations\\s+of|Obligations?|Next\\s+Obligation(\\s+of)?|Final\\s+Obligation(\\s+of)?|Solve\\s+Obligations(\\s+of)?|Solve\\s+All\\s+Obligations|Admit\\s+Obligations(\\s+of)?|Instance)\\b",
"comment": "Obligations",
"captures": {
"1": {
Expand All @@ -76,7 +88,7 @@
}
},
{
"match": "(CoInductive|Inductive|Variant|Record|Structure|Class)\\s+(>\\s*)?((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"match": "\\b(CoInductive|Inductive|Variant|Record|Structure|Class)\\s+(>\\s*)?((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Type declarations",
"captures": {
"1": {
Expand All @@ -88,7 +100,7 @@
}
},
{
"match": "(Ltac)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"match": "\\b(Ltac)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)",
"comment": "Ltac declarations",
"captures": {
"1": {
Expand All @@ -100,20 +112,119 @@
}
},
{
"match": "\\b(Hint|Constructors|Resolve|Rewrite|Ltac|Implicit(\\s+Types)?|Set|Unset|Remove\\s+Printing|Arguments|Tactic\\s+Notation|Notation|Infix|Reserved\\s+Notation|Section|Module\\s+Type|Module|End|Check|Print|Eval|Search|Universe|Coercions?|Generalizable\\s+All|Generalizable\\s+Variable?|Existing\\s+Instance|Existing\\s+Class|Canonical|About|Locate|Collection|Typeclasses\\s+(Opaque|Transparent)|Reset(\\s+Initial)?|Back)\\b",
"match": "\\b(Constructors|Resolve|Rewrite|Ltac|Implicit(\\s+Types?)?|Set|Unset|Remove\\s+Printing|Arguments|Tactic\\s+Notation|(String\\s+|Number\\s+)?Notation|Infix|Reserved\\s+Infix|Reserved\\s+Notation|(Enable|Disable)\\s+Notation|Section|Module\\s+Type|Module|End|Check|Eval|Search|Universes?|(Identity\\s+)?Coercions?|Generalizable\\s+All\\s+Variables|Generalizable\\s+No\\s+Variables|Generalizable\\s+Variables?|Existing\\s+Instances?|Existing\\s+Class|Canonical|About|Collection|Typeclasses|Opaque|Transparent|Test|Pwd|Cd|Back|BackTo|Strategy|SearchAbout|SearchHead|SearchPattern|SearchRewrite|Create\\s+HintDb|Comments|Compute|Combined\\s+Scheme|Constraint|Preterm|Prenex\\s+Implicits|Optimize\\s+Heap|Optimize\\s+Proof|Inspect|Guarded|Validate\\s+Proof|Attributes|Register(\\s+Inline|Scheme)?)\\b",
"comment": "Vernacular keywords",
"name": "keyword.source.coq"
},
{
"match": "\\b(Proof|Qed|Defined|Save|Abort(\\s+All)?|Undo(\\s+To)?|Restart|Focus|Unfocus|Unfocused|Show\\s+Proof|Show\\s+Existentials|Show|Unshelve)\\b",
"match": "\\b(Hint(\\s+(Constants|Constructors|Cut|Extern|Immediate|Mode|Opaque|Projections|Resolve|Rewrite|Transparent|Unfold|Variables|(View\\s+for\\s+(apply|move))))?)\\b",
"comment": "Vernacular Hint commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Print(\\s+(All(\\s+Dependencies)?|Assumptions|Canonical\\s+Projections|Classes|Coercion\\s+Paths|Coercions|Custom\\s+Grammar|Debug\\s+GC|Equivalent\\s+Keys|Extraction\\s+Blacklist|Extraction\\s+Inline|Fields|Firstorder\\s+Solver|Grammar|Graph|Hint|HintDb|Implicit|Instances|Keywords|Libraries|LoadPath|Ltac(\\s+Signatures)?|Ltac2(\\s+(Signatures|Type))?|ML\\s+Modules|ML\\s+Path|Module(\\s+Type)?|Namespace|Notation|Opaque\\s+Dependencies|Options|Registered|Rewrite\\s+HintDb|Rings|Scope|Scopes|Strategy|Section|Strategies|Tables?|Term|Transparent\\s+Dependencies|Typing\\s+Flags|Universes|Universes\\s+Subgraph|Visibility))?)\\b",
"comment": "Vernacular Print commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Add(\\s+(Field|LoadPath|ML\\s+Path|Morphism|Parametric\\s+Morphism|Parametric\\s+Relation|Parametric\\s+Setoid|Rec\\s+LoadPath|Relation|Ring|Setoid|Zify))?)\\b",
"comment": "Vernacular Add commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Ltac2(\\s+(Eval|External|Globalize|Notation|Set|Type))?)\\b",
"comment": "Vernacular Ltac2 commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Remove(\\s+(Hints|LoadPath))?)\\b",
"comment": "Vernacular Remove commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Reset(\\s+(Extraction\\s+Blacklist|Extraction\\s+Inline|Initial|Ltac\\s+Profile))?)\\b",
"comment": "Vernacular Reset commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Locate(\\s+(File|Library|Ltac|Ltac2|Module|Term))?)\\b",
"comment": "Vernacular Locate commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Declare\\s+(Custom\\s+Entry|Equivalent\\s+Keys|Instance|Left\\s+Step|Module|ML\\s+Module|Morphism|Reduction|Right\\s+Step|Scope))\\b",
"comment": "Vernacular Declare commands",
"name": "keyword.control.import.coq"
},
{
"match": "\\b(Show(\\s+(Conjectures|Existentials|Extraction|Goal|Intros?|Lia\\s+Profile|Ltac\\s+Profile|Match|Obligation\\s+Tactic|Proof|Script|Universes|Zify))?)\\b",
"comment": "Vernacular Show commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Proof(\\s+(Mode|using|with))?|Qed|Defined|Save|Abort(\\s+All)?|Undo(\\s+To)?|Restart|Focus|Unfocus|Unfocused|Unshelve)\\b",
"comment": "Proof keywords",
"name": "keyword.source.coq"
},
{
"match": "\\b(Quit|Drop|Time|Redirect|Timeout|Fail)\\b",
"match": "\\b(Extract\\s+(Constant|Inductive|Inlined\\s+Constant)|Separate\\s+Extraction|Recursive\\s+Extraction(\\s+Library)?|Extraction(\\s+(Blacklist|Implicit|Inline|Language(\\s+(OCaml|Haskell|Scheme|JSON))?|Library|NoInline|TestCompile))?)\\b",
"comment": "Extraction commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Quit|Drop|Time|Redirect|Timeout|Fail|Succeed|Info|Instructions)\\b",
"comment": "Vernacular Debug keywords",
"name": "keyword.debug.coq"
},
{
"match": "\\b(Debug\\s+(On|Off))\\b",
"comment": "Vernacular Debug keywords",
"name": "keyword.debug.coq"
},
{
"match": "\\b(Derive)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)\\s+(SuchThat)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)\\s+(As)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)\\b",
"comment": "Vernacular Derive command",
"captures": {
"1": {
"name": "keyword.source.coq"
},
"2": {
"name": "entity.name.function.theorem.coq"
},
"5": {
"name": "keyword.source.coq"
},
"6": {
"name": "entity.name.function.theorem.coq"
},
"9": {
"name": "keyword.source.coq"
},
"10": {
"name": "entity.name.function.theorem.coq"
}
}
},
{
"match": "\\b(Derive\\s+((Dependent)\\s+)?(Inversion|Inversion_clear))\\b",
"comment": "Vernacular Derive Inversion commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Functional\\s+Scheme|Functional\\s+Case|Generate\\s+graph\\s+for)\\b",
"comment": "Vernacular Functional Induction commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Scheme(\\s+(Boolean\\s+)?Equality\\s+for)?)\\b",
"comment": "Vernacular Scheme commands",
"name": "keyword.source.coq"
},
{
"match": "\\b(Polymorphic|Monomorphic|Cumulative|NonCumulative|Private)\\b",
"comment": "Legacy attributes",
"name": "keyword.source.coq"
},
{
"match": "\\b(admit|Admitted)\\b",
"comment": "Admits are bad",
Expand All @@ -125,7 +236,7 @@
"name": "keyword.operator.coq"
},
{
"match": "\\b(forall|exists|Type|Set|Prop|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\b|∀|∃",
"match": "\\b(forall|exists|Type|Set|Prop|SProp|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\b|∀|∃",
"comment": "Type keywords",
"name": "support.type.coq"
},
Expand All @@ -145,7 +256,7 @@
"name": "keyword.control.gallina"
},
{
"match": "\\b(intro|intros|revert|induction|destruct|auto|eauto|tauto|eassumption|apply|eapply|assumption|constructor|econstructor|reflexivity|inversion|injection|assert|split|esplit|omega|fold|unfold|specialize|rewrite|erewrite|change|symmetry|refine|simpl|intuition|firstorder|generalize|idtac|exist|exists|eexists|elim|eelim|rename|subst|congruence|trivial|left|right|set|pose|discriminate|clear|clearbody|contradict|contradiction|exact|dependent|remember|case|easy|unshelve|pattern|transitivity|etransitivity|f_equal|exfalso|replace|abstract|cycle|swap|revgoals|shelve|unshelve)\\b",
"match": "\\b(intro|intros|revert|induction|destruct|auto|eauto|tauto|eassumption|apply|eapply|assumption|constructor|econstructor|reflexivity|inversion|injection|assert|split|esplit|omega|fold|unfold|specialize|rewrite|erewrite|change|symmetry|refine|simpl|intuition|firstorder|generalize|idtac|exist|exists|eexists|elim|eelim|rename|subst|congruence|trivial|left|right|set|pose|discriminate|clear|clearbody|contradict|contradiction|exact|dependent|remember|case|easy|unshelve|pattern|transitivity|etransitivity|f_equal|exfalso|replace|abstract|cycle|swap|revgoals|shelve|unshelve|typeclasses\\s+eauto)\\b",
"comment": "Ltac builtins",
"name": "support.function.builtin.ltac"
},
Expand Down