@@ -0,0 +1,125 @@
1+%YAML 1.2
2+---
3+# http://www.sublimetext.com/docs/3/syntax.html
4+name: Lean
5+file_extensions:
6+ - lean
7+scope: source.lean
8+contexts:
9+ main:
10+ - include: comments
11+ - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\b\s+(\{[^}]*\})?'
12+ captures:
13+ 1: keyword.other.definitioncommand.lean
14+ push:
15+ - meta_scope: meta.definitioncommand.lean
16+ - match: '(?=\bwith\b|\bextends\b|[:\|\(\[\{⦃<>])'
17+ pop: true
18+ - include: comments
19+ - include: definitionName
20+ - match: ","
21+ - match: \b(Prop|Type|Sort)\b
22+ scope: storage.type.lean
23+ - match: '\battribute\b\s*\[[^\]]*\]'
24+ scope: storage.modifier.lean
25+ - match: '@\[[^\]]*\]'
26+ scope: storage.modifier.lean
27+ - match: \b(?<!\.)(private|meta|mutual|protected|noncomputable)\b
28+ scope: keyword.control.definition.modifier.lean
29+ - match: \b(sorry)\b
30+ scope: invalid.illegal.lean
31+ - match: '#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b'
32+ scope: keyword.other.command.lean
33+ - match: '#(print|eval|reduce|check|help|exit|find|where)\b'
34+ scope: keyword.other.command.lean
35+ - 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
36+ scope: keyword.other.lean
37+ - match: \b(?<!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\.)\b
38+ scope: keyword.other.lean
39+ - match: «
40+ push:
41+ - meta_content_scope: entity.name.lean
42+ - match: »
43+ pop: true
44+ - match: \b(?<!\.)(if|then|else)\b
45+ scope: keyword.control.lean
46+ - match: '"'
47+ captures:
48+ 0: punctuation.definition.string.begin.lean
49+ push:
50+ - meta_scope: string.quoted.double.lean
51+ - match: '"'
52+ captures:
53+ 0: punctuation.definition.string.end.lean
54+ pop: true
55+ - match: '\\[\\"nt'']'
56+ scope: constant.character.escape.lean
57+ - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
58+ scope: constant.character.escape.lean
59+ - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
60+ scope: constant.character.escape.lean
61+ - match: '''[^\\'']'''
62+ scope: string.quoted.single.lean
63+ - match: '''(\\(x..|u....|.))'''
64+ scope: string.quoted.single.lean
65+ captures:
66+ 1: constant.character.escape.lean
67+ - match: '`+[^\[(]\S+'
68+ scope: entity.name.lean
69+ - match: '\b([0-9]+|0([xX][0-9a-fA-F]+))\b'
70+ scope: constant.numeric.lean
71+ blockComment:
72+ - match: /-
73+ push:
74+ - meta_scope: comment.block.lean
75+ - match: "-/"
76+ pop: true
77+ - include: scope:source.lean.markdown
78+ - include: blockComment
79+ comments:
80+ - include: dashComment
81+ - include: docComment
82+ - include: stringBlock
83+ - include: modDocComment
84+ - include: blockComment
85+ dashComment:
86+ - match: (--)
87+ captures:
88+ 0: punctuation.definition.comment.lean
89+ push:
90+ - meta_scope: comment.line.double-dash.lean
91+ - match: $
92+ pop: true
93+ - include: scope:source.lean.markdown
94+ definitionName:
95+ - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*'
96+ scope: entity.name.function.lean
97+ - match: «
98+ push:
99+ - meta_content_scope: entity.name.function.lean
100+ - match: »
101+ pop: true
102+ docComment:
103+ - match: /--
104+ push:
105+ - meta_scope: comment.block.documentation.lean
106+ - match: "-/"
107+ pop: true
108+ - include: scope:source.lean.markdown
109+ - include: blockComment
110+ modDocComment:
111+ - match: /-!
112+ push:
113+ - meta_scope: comment.block.documentation.lean
114+ - match: "-/"
115+ pop: true
116+ - include: scope:source.lean.markdown
117+ - include: blockComment
118+ stringBlock:
119+ - match: /-"
120+ push:
121+ - meta_scope: comment.block.string.lean
122+ - match: '"-/'
123+ pop: true
124+ - include: scope:source.lean.markdown
125+ - include: blockComment