diff options
author | Julian Berman <Julian@GrayVines.com> | 2020-12-21 13:08:20 -0500 |
---|---|---|
committer | David Peter <sharkdp@users.noreply.github.com> | 2021-01-02 09:45:19 +0100 |
commit | 1a04dcf10f502798c7907cb1e1da37d5b8955eb8 (patch) | |
tree | 9dd38d9c4ec2527e913af2c2812051a381f49387 /assets | |
parent | 2eae8b578edb21918b0417a8d4cc334dfd13fb48 (diff) |
Add Lean.sublime-syntax.
Covers syntax for Lean 3, an interactive theorem prover
at https://leanprover-community.github.io/ whose users
mostly use VSCode.
Diffstat (limited to 'assets')
-rw-r--r-- | assets/syntaxes/02_Extra/Lean.sublime-syntax | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/assets/syntaxes/02_Extra/Lean.sublime-syntax b/assets/syntaxes/02_Extra/Lean.sublime-syntax new file mode 100644 index 00000000..55e47cdd --- /dev/null +++ b/assets/syntaxes/02_Extra/Lean.sublime-syntax @@ -0,0 +1,125 @@ +%YAML 1.2 +--- +# http://www.sublimetext.com/docs/3/syntax.html +name: Lean +file_extensions: + - lean +scope: source.lean +contexts: + main: + - include: comments + - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\b\s+(\{[^}]*\})?' + captures: + 1: keyword.other.definitioncommand.lean + push: + - meta_scope: meta.definitioncommand.lean + - match: '(?=\bwith\b|\bextends\b|[:\|\(\[\{⦃<>])' + pop: true + - include: comments + - include: definitionName + - match: "," + - match: \b(Prop|Type|Sort)\b + scope: storage.type.lean + - match: '\battribute\b\s*\[[^\]]*\]' + scope: storage.modifier.lean + - match: '@\[[^\]]*\]' + scope: storage.modifier.lean + - match: \b(?<!\.)(private|meta|mutual|protected|noncomputable)\b + scope: keyword.control.definition.modifier.lean + - match: \b(sorry)\b + scope: invalid.illegal.lean + - match: '#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b' + scope: keyword.other.command.lean + - match: '#(print|eval|reduce|check|help|exit|find|where)\b' + scope: keyword.other.command.lean + - match: \b(?<!\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\.)\b + scope: keyword.other.lean + - match: \b(?<!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\.)\b + scope: keyword.other.lean + - match: « + push: + - meta_content_scope: entity.name.lean + - match: » + pop: true + - match: \b(?<!\.)(if|then|else)\b + scope: keyword.control.lean + - match: '"' + captures: + 0: punctuation.definition.string.begin.lean + push: + - meta_scope: string.quoted.double.lean + - match: '"' + captures: + 0: punctuation.definition.string.end.lean + pop: true + - match: '\\[\\"nt'']' + scope: constant.character.escape.lean + - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]' + scope: constant.character.escape.lean + - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]' + scope: constant.character.escape.lean + - match: '''[^\\'']''' + scope: string.quoted.single.lean + - match: '''(\\(x..|u....|.))''' + scope: string.quoted.single.lean + captures: + 1: constant.character.escape.lean + - match: '`+[^\[(]\S+' + scope: entity.name.lean + - match: '\b([0-9]+|0([xX][0-9a-fA-F]+))\b' + scope: constant.numeric.lean + blockComment: + - match: /- + push: + - meta_scope: comment.block.lean + - match: "-/" + pop: true + - include: scope:source.lean.markdown + - include: blockComment + comments: + - include: dashComment + - include: docComment + - include: stringBlock + - include: modDocComment + - include: blockComment + dashComment: + - match: (--) + captures: + 0: punctuation.definition.comment.lean + push: + - meta_scope: comment.line.double-dash.lean + - match: $ + pop: true + - include: scope:source.lean.markdown + definitionName: + - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*' + scope: entity.name.function.lean + - match: « + push: + - meta_content_scope: entity.name.function.lean + - match: » + pop: true + docComment: + - match: /-- + push: + - meta_scope: comment.block.documentation.lean + - match: "-/" + pop: true + - include: scope:source.lean.markdown + - include: blockComment + modDocComment: + - match: /-! + push: + - meta_scope: comment.block.documentation.lean + - match: "-/" + pop: true + - include: scope:source.lean.markdown + - include: blockComment + stringBlock: + - match: /-" + push: + - meta_scope: comment.block.string.lean + - match: '"-/' + pop: true + - include: scope:source.lean.markdown + - include: blockComment |