diff --git a/CHANGES.md b/CHANGES.md index 8dbfea240..d340530cd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -10,6 +10,7 @@ - Use plugin include paths from `_CoqProject` (@ejgallego, #88) - Support OCaml >= 4.12 (@ejgallego, #93) - Optimize the number of diagnostics sent in eager mode (@ejgallego, #104) + - Improved syntax highlighting (@artagnon, #105) # coq-lsp 0.1.0: Memory ----------------------- diff --git a/editor/code/package.json b/editor/code/package.json index c141a6360..eed1727ba 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -53,7 +53,7 @@ { "language": "coq", "scopeName": "source.coq", - "path": "./syntaxes/coq.tmLanguage" + "path": "./syntaxes/coq.json" } ], "commands": [ diff --git a/editor/code/syntaxes/coq.json b/editor/code/syntaxes/coq.json new file mode 100644 index 000000000..ef30e6c04 --- /dev/null +++ b/editor/code/syntaxes/coq.json @@ -0,0 +1,229 @@ +{ + "fileTypes": ["v"], + "name": "Coq", + "patterns": [ + { + "match": "\\b(From|Require|Import|Export|Local|Global|Include)\\b", + "comment": "Vernacular import keywords", + "name": "keyword.control.import.coq" + }, + { + "match": "\\b((Open|Close|Delimit|Undelimit|Bind)\\s+Scope)\\b", + "comment": "Vernacular scope keywords", + "name": "keyword.control.import.coq" + }, + { + "match": "(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition|Goal)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", + "comment": "Theorem declarations", + "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", + "captures": { + "1": { + "name": "keyword.source.coq" + }, + "2": { + "name": "keyword.source.coq" + }, + "3": { + "name": "entity.name.assumption.coq" + } + } + }, + { + "match": "\\b(Context)\\b\\s*`?\\s*(\\(|\\{)?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", + "comment": "Context", + "captures": { + "1": { + "name": "keyword.source.coq" + }, + "3": { + "name": "entity.name.assumption.coq" + } + } + }, + { + "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'])*)", + "comment": "Definitions", + "captures": { + "1": { + "name": "keyword.source.coq" + }, + "2": { + "name": "keyword.source.coq" + }, + "3": { + "name": "entity.name.function.coq" + } + } + }, + { + "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", + "comment": "Obligations", + "captures": { + "1": { + "name": "keyword.source.coq" + } + } + }, + { + "match": "(CoInductive|Inductive|Variant|Record|Structure|Class)\\s+(>\\s*)?((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", + "comment": "Type declarations", + "captures": { + "1": { + "name": "keyword.source.coq" + }, + "3": { + "name": "entity.name.type.coq" + } + } + }, + { + "match": "(Ltac)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", + "comment": "Ltac declarations", + "captures": { + "1": { + "name": "keyword.source.coq" + }, + "2": { + "name": "entity.name.function.ltac" + } + } + }, + { + "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))\\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", + "comment": "Proof keywords", + "name": "keyword.source.coq" + }, + { + "match": "\\b(Quit|Drop|Time|Redirect|Timeout|Fail)\\b", + "comment": "Vernacular Debug keywords", + "name": "keyword.debug.coq" + }, + { + "match": "\\b(admit|Admitted)\\b", + "comment": "Admits are bad", + "name": "invalid.illegal.admit.coq" + }, + { + "match": ":|\\||=|<|>|\\*|\\+|-|\\{|\\}|≠|∨|∧|↔|¬|→|≤|≥", + "comment": "Operators", + "name": "keyword.operator.coq" + }, + { + "match": "\\b(forall|exists|Type|Set|Prop|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\b|∀|∃", + "comment": "Type keywords", + "name": "support.type.coq" + }, + { + "match": "\\b(try|repeat|rew|progress|fresh|solve|now|first|tryif|at|once|do|only)\\b", + "comment": "Ltac keywords", + "name": "keyword.control.ltac" + }, + { + "match": "\\b(into|with|eqn|by|move|as|using)\\b", + "comment": "Common Ltac connectors", + "name": "keyword.control.ltac" + }, + { + "match": "\\b(match|lazymatch|multimatch|fun|with|return|end|let|in|if|then|else|fix|for|where|and)\\b|λ", + "comment": "Gallina keywords", + "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", + "comment": "Ltac builtins", + "name": "support.function.builtin.ltac" + }, + { + "applyEndPatternLast": 1, + "begin": "\\(\\*(?!#)", + "end": "\\*\\)", + "name": "comment.block.coq", + "patterns": [ + { + "include": "#block_comment" + }, + { + "include": "#block_double_quoted_string" + } + ] + }, + { + "match": "\\b((0(x|X)[0-9a-fA-F]+)|([0-9]+(\\.[0-9]+)?))\\b", + "name": "constant.numeric.gallina" + }, + { + "match": "\\b(True|False|tt|false|true|Some|None|nil|cons|pair|inl|inr|O|S|Eq|Lt|Gt|id|ex|all|unique)\\b", + "comment": "Gallina builtin constructors", + "name": "constant.language.constructor.gallina" + }, + { + "match": "\\b_\\b", + "name": "constant.language.wildcard.coq" + }, + { + "begin": "\"", + "beginCaptures": { + "0": { + "name": "punctuation.definition.string.begin.coq" + } + }, + "end": "\"", + "endCaptures": { + "0": { + "name": "punctuation.definition.string.end.coq" + } + }, + "name": "string.quoted.double.coq" + } + ], + "repository": { + "block_comment": { + "applyEndPatternLast": 1, + "begin": "\\(\\*(?!#)", + "end": "\\*\\)", + "name": "comment.block.coq", + "patterns": [ + { + "include": "#block_comment" + }, + { + "include": "#block_double_quoted_string" + } + ] + }, + "block_double_quoted_string": { + "applyEndPatternLast": 1, + "begin": "\"", + "beginCaptures": { + "0": { + "name": "punctuation.definition.string.begin.coq" + } + }, + "end": "\"", + "endCaptures": { + "0": { + "name": "punctuation.definition.string.end.coq" + } + }, + "name": "string.quoted.double.coq" + } + }, + "scopeName": "source.coq", + "uuid": "CDE1AD3A-C094-457D-B321-93009C6BCFDA" +} diff --git a/editor/code/syntaxes/coq.tmLanguage b/editor/code/syntaxes/coq.tmLanguage deleted file mode 100644 index 9a722e4e6..000000000 --- a/editor/code/syntaxes/coq.tmLanguage +++ /dev/null @@ -1,342 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd"> -<plist version="1.0"> - <dict> - <key>fileTypes</key> - <array> - <string>v</string> - </array> - <!-- <key>foldingStartMarker</key> - <string>(?x: # turn on extended mode - ^ # a line beginning with - \s* # some optional space - [{\[] # the start of an object or array - (?! # but not followed by - .* # whatever - [}\]] # and the close of an object or array - ,? # an optional comma - \s* # some optional space - $ # at the end of the line - ) - | # ...or... - [{\[] # the start of an object or array - \s* # some optional space - $ # at the end of the line - )</string> - <key>foldingStopMarker</key> - <string>(?x: # turn on extended mode - ^ # a line beginning with - \s* # some optional space - [}\]] # and the close of an object or array - )</string> --> - <key>name</key> - <string>Coq</string> - <key>patterns</key> - <array> - - <dict> - <key>match</key> - <string>\b(Require|Import|Export|Local|Global|Open|Scope)\b</string> - <key>comment</key> - <string>Vernacular import keywords</string> - <key>name</key> - <string>keyword.control.import.coq</string> - </dict> - - <dict> - <key>match</key> - <string>(Lemma|Theorem|Goal|Example)\s+([a-zA-Z][a-zA-Z0-9_']*)</string> - <key>comment</key> - <string>Theorem declarations</string> - <key>captures</key> - <dict> - <key>1</key> - <dict> - <key>name</key> - <string>keyword.source.coq</string> - </dict> - <key>2</key> - <dict> - <key>name</key> - <string>entity.name.function.theorem.coq</string> - </dict> - </dict> - </dict> - - <dict> - <key>match</key> - <string>(Program Definition|Program Fixpoint|Program CoFixpoint|Program Function|Function|CoFixpoint|Fixpoint|Definition|Let)\s+([a-zA-Z_][a-zA-Z0-9_']*)</string> - <key>comment</key> - <string>Definitions</string> - <key>captures</key> - <dict> - <key>1</key> - <dict> - <key>name</key> - <string>keyword.source.coq</string> - </dict> - <key>2</key> - <dict> - <key>name</key> - <string>entity.name.function.coq</string> - </dict> - </dict> - </dict> - - <dict> - <key>match</key> - <string>(CoInductive|Inductive)\s+([a-zA-Z][a-zA-Z0-9_']*)</string> - <key>comment</key> - <string>Inductive type declarations</string> - <key>captures</key> - <dict> - <key>1</key> - <dict> - <key>name</key> - <string>keyword.source.coq</string> - </dict> - <key>2</key> - <dict> - <key>name</key> - <string>entity.name.type.coq</string> - </dict> - </dict> - </dict> - - <dict> - <key>match</key> - <string>(Ltac)\s+([a-zA-Z][a-zA-Z0-9_']*)</string> - <key>comment</key> - <string>Ltac declarations</string> - <key>captures</key> - <dict> - <key>1</key> - <dict> - <key>name</key> - <string>keyword.source.coq</string> - </dict> - <key>2</key> - <dict> - <key>name</key> - <string>entity.name.function.ltac</string> - </dict> - </dict> - </dict> - - <dict> - <key>match</key> - <string>\b(Hint|Constructors|Resolve|Rewrite|Proof|Ltac|Qed|Defined|Implicit|Set|Unset|Arguments|Tactic Notation|Notation|Section|Module Type|Module|End|Variables|Record|Check|Print|Eval)\b</string> - <key>comment</key> - <string>Vernacular keywords</string> - <key>name</key> - <string>keyword.source.coq</string> - </dict> - - <dict> - <key>match</key> - <string>\b(admit|Admitted)\b</string> - <key>comment</key> - <string>Admits are bad</string> - <key>name</key> - <string>invalid.illegal.admit.coq</string> - </dict> - - <dict> - <key>match</key> - <string>:|\||=|<|>|\*|\+|-|\{|\}</string> - <key>comment</key> - <string>Operators</string> - <key>name</key> - <string>keyword.operator.coq</string> - </dict> - - <dict> - <key>match</key> - <string>\b(forall|exists|Type|Set|Prop)\b</string> - <key>comment</key> - <string>Type keywords</string> - <key>name</key> - <string>support.type.coq</string> - </dict> - - <dict> - <key>match</key> - <string>\b(try|repeat|progress|set|fresh|solve|now|first)\b</string> - <key>comment</key> - <string>Ltac keywords</string> - <key>name</key> - <string>keyword.control.ltac</string> - </dict> - - <dict> - <key>match</key> - <string>\b(into|with|eqn|by|as|using)\b</string> - <key>comment</key> - <string>Common Ltac connectors</string> - <key>name</key> - <string>keyword.control.ltac</string> - </dict> - - <dict> - <key>match</key> - <string>\b(match|lazymatch|multimatch|fun|with|returns|end|let|in|if|then|else)\b</string> - <key>comment</key> - <string>Gallina keywords</string> - <key>name</key> - <string>keyword.control.gallina</string> - </dict> - - <dict> - <key>match</key> - <string>\b(intro|intros|induction|destruct|auto|eauto|eassumption|apply|eapply|assumption|constructor|econstructor|reflexivity|inversion|assert|split|omega|fold|unfold|specialize|rewrite|erewrite|symmetry|refine|simpl|intuition|firstorder|generalize|idtac|exist|exists|eexists|elim|eelim|rename|subst|congruence|trivial|left|right|pose|discriminate|clear|clearbody|contradict|contradiction|exact|dependent|remember)\b</string> - <key>comment</key> - <string>Ltac builtins</string> - <key>name</key> - <string>support.function.builtin.ltac</string> - </dict> - - <dict> - <key>applyEndPatternLast</key> - <integer>1</integer> - <key>begin</key> - <string>\(\*(?!#)</string> - <key>end</key> - <string>\*\)</string> - <key>name</key> - <string>comment.block.coq</string> - <key>patterns</key> - <array> - <dict> - <key>include</key> - <string>#block_comment</string> - </dict> - <dict> - <key>include</key> - <string>#block_double_quoted_string</string> - </dict> - </array> - </dict> - - <dict> - <key>match</key> - <string>\bnil\b</string> - <key>name</key> - <string>constant.language.nil.gallina</string> - </dict> - - <dict> - <key>match</key> - <string>\b((0(x|X)[0-9a-fA-F]+)|([0-9]+(\.[0-9]+)?))\b</string> - <key>name</key> - <string>constant.numeric.gallina</string> - </dict> - - <dict> - <key>match</key> - <string>\bTrue\b</string> - <key>name</key> - <string>constant.language.boolean.true.gallina</string> - </dict> - - <dict> - <key>match</key> - <string>\bFalse\b</string> - <key>name</key> - <string>constant.language.boolean.false.gallina</string> - </dict> - - <dict> - <key>match</key> - <string>\b_\b</string> - <key>name</key> - <string>constant.language.wildcard.coq</string> - </dict> - - <dict> - <key>begin</key> - <string>"</string> - <key>beginCaptures</key> - <dict> - <key>0</key> - <dict> - <key>name</key> - <string>punctuation.definition.string.begin.coq</string> - </dict> - </dict> - <key>end</key> - <string>"</string> - <key>endCaptures</key> - <dict> - <key>0</key> - <dict> - <key>name</key> - <string>punctuation.definition.string.end.coq</string> - </dict> - </dict> - <key>name</key> - <string>string.quoted.double.coq</string> - </dict> - - </array> - - <key>repository</key> - <dict> - <key>block_comment</key> - <dict> - <key>applyEndPatternLast</key> - <integer>1</integer> - <key>begin</key> - <string>\(\*(?!#)</string> - <key>end</key> - <string>\*\)</string> - <key>name</key> - <string>comment.block.coq</string> - <key>patterns</key> - <array> - <dict> - <key>include</key> - <string>#block_comment</string> - </dict> - <dict> - <key>include</key> - <string>#block_double_quoted_string</string> - </dict> - </array> - </dict> - - <key>block_double_quoted_string</key> - <dict> - <key>applyEndPatternLast</key> - <integer>1</integer> - <key>begin</key> - <string>"</string> - <key>beginCaptures</key> - <dict> - <key>0</key> - <dict> - <key>name</key> - <string>punctuation.definition.string.begin.coq</string> - </dict> - </dict> - <key>end</key> - <string>"</string> - <key>endCaptures</key> - <dict> - <key>0</key> - <dict> - <key>name</key> - <string>punctuation.definition.string.end.coq</string> - </dict> - </dict> - <key>name</key> - <string>string.quoted.double.coq</string> - </dict> - - </dict> - - <key>scopeName</key> - <string>source.coq</string> - <key>uuid</key> - <string>CDE1AD3A-C094-457D-B321-93009C6BCFDA</string> - </dict> -</plist>