/
source.idris.js
317 lines (316 loc) · 11 KB
/
source.idris.js
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
// This is a TextMate grammar distributed by `starry-night`.
// This grammar is developed at
// <https://github.com/idris-hackers/idris-sublime>
// and licensed `mit`.
// See <https://github.com/wooorm/starry-night> for more info.
/** @type {import('../lib/index.js').Grammar} */
const grammar = {
extensions: ['.idr', '.lidr'],
names: ['idris'],
patterns: [
{
captures: {
1: {name: 'punctuation.definition.entity.idris'},
2: {name: 'punctuation.definition.entity.idris'}
},
match: "(`)[\\w']*?(`)",
name: 'keyword.operator.function.infix.idris'
},
{
captures: {1: {name: 'keyword.other.idris'}},
match: "^(module)\\s+([a-zA-Z0-9._']+)$",
name: 'meta.declaration.module.idris'
},
{
captures: {1: {name: 'keyword.other.idris'}},
match: "^(import)\\s+([a-zA-Z0-9._']+)$",
name: 'meta.import.idris'
},
{
match: '\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b',
name: 'constant.numeric.float.idris'
},
{
match: '\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b',
name: 'constant.numeric.idris'
},
{
match: '^\\b(public|abstract|private)\\b',
name: 'storage.modifier.export.idris'
},
{match: '\\b(total|partial)\\b', name: 'storage.modifier.totality.idris'},
{match: '^\\b(implicit)\\b', name: 'storage.modifier.idris'},
{
begin: '\\"',
beginCaptures: {0: {name: 'punctuation.definition.string.begin.idris'}},
end: '\\"',
endCaptures: {0: {name: 'punctuation.definition.string.end.idris'}},
name: 'string.quoted.double.idris',
patterns: [{include: '#escape_characters'}]
},
{
begin: "(?<!\\w)\\'",
beginCaptures: {0: {name: 'punctuation.definition.string.begin.idris'}},
end: "\\'",
endCaptures: {0: {name: 'punctuation.definition.string.end.idris'}},
name: 'string.quoted.single.idris',
patterns: [
{include: '#escape_characters'},
{match: '\\n', name: 'invalid.illegal.idris'}
]
},
{
begin: '\\b(class)\\b',
beginCaptures: {1: {name: 'keyword.other.idris'}},
end: '\\b(where)\\b|$',
endCaptures: {1: {name: 'keyword.other.idris'}},
name: 'meta.declaration.class.idris',
patterns: [{include: '#prelude_class'}, {include: '#prelude_type'}]
},
{
begin: '\\b(instance)\\b',
beginCaptures: {1: {name: 'keyword.other.idris'}},
end: '\\b(where)\\b|$',
endCaptures: {1: {name: 'keyword.other.idris'}},
name: 'meta.declaration.instance.idris',
patterns: [
{include: '#prelude_class'},
{include: '#prelude_type'},
{include: '#context_signature'},
{include: '#type_signature'}
]
},
{
begin: "\\b(data)\\s+([\\w']+)\\s*(:)?",
beginCaptures: {
1: {name: 'keyword.other.idris'},
2: {name: 'entity.name.type.idris'},
3: {name: 'keyword.operator.colon.idris'}
},
end: '\\b(where)\\b|(=)',
endCaptures: {
1: {name: 'keyword.other.idris'},
2: {name: 'keyword.operator.idris'}
},
name: 'meta.declaration.data.idris',
patterns: [{include: '#type_signature'}]
},
{include: '#function_signature'},
{include: '#directive'},
{include: '#comments'},
{include: '#language_const'},
{include: '#language_keyword'},
{include: '#prelude'},
{match: "\\b[A-Z][A-Za-z_'0-9]*", name: 'constant.other.idris'},
{match: '[|&!%$?~+:\\-.=</>\\\\*]+', name: 'keyword.operator.idris'},
{match: ',', name: 'punctuation.separator.comma.idris'}
],
repository: {
block_comment: {
begin: '\\{-(?!#)',
captures: {0: {name: 'punctuation.definition.comment.idris'}},
end: '-\\}',
name: 'comment.block.idris',
patterns: [{include: '#block_comment'}]
},
comments: {
patterns: [
{
captures: {1: {name: 'punctuation.definition.comment.idris'}},
match: '(--).*$\\n?',
name: 'comment.line.double-dash.idris'
},
{
captures: {1: {name: 'punctuation.definition.comment.idris'}},
match: '(\\|\\|\\|).*$\\n?',
name: 'comment.line.triple-bar.idris'
},
{include: '#block_comment'}
]
},
context_signature: {
patterns: [
{
captures: {
1: {name: 'entity.other.inherited-class.idris'},
2: {name: 'entity.other.attribute-name.idris'},
4: {name: 'keyword.operator.double-arrow.idris'}
},
match: "([\\w._']+)((\\s+[\\w_']+)+)\\s*(=>)",
name: 'meta.context-signature.idris'
},
{
begin: '(\\()((?=.*\\)\\s*=>)|(?=[^)]*$))',
beginCaptures: {1: {name: 'punctuation.context.begin.idris'}},
end: '(\\))\\s*(=>)',
endCaptures: {
1: {name: 'punctuation.context.end.idris'},
2: {name: 'keyword.operator.double-arrow.idris'}
},
name: 'meta.context-signature.idris',
patterns: [
{
captures: {
1: {name: 'entity.other.inherited-class.idris'},
2: {name: 'entity.other.attribute-name.idris'}
},
match: "([\\w']+)\\s+([\\w']+)",
name: 'meta.class-constraint.idris'
}
]
}
]
},
directive: {
patterns: [
{
captures: {
1: {name: 'keyword.other.directive.idris'},
2: {name: 'keyword.other.language-extension.idris'}
},
match: '^%(language)\\s+(.*)$',
name: 'meta.directive.language-extension.idris'
},
{
captures: {
1: {name: 'keyword.other.directive.idris'},
2: {name: 'keyword.other.totality.idris'}
},
match: '^%(default)\\s+(total|partial)$',
name: 'meta.directive.totality.idris'
},
{
captures: {
1: {name: 'keyword.other.directive.idris'},
2: {name: 'keyword.other.idris'}
},
match: '^%(provide)\\s+.*\\s+(with)\\s+.*$',
name: 'meta.directive.type-provider.idris'
},
{
captures: {
1: {name: 'keyword.other.directive.idris'},
2: {name: 'storage.modifier.export.idris'}
},
match: '^%(access)\\s+(public|abstract|private)$',
name: 'meta.directive.export.idris'
},
{
captures: {1: {name: 'keyword.other.directive.idris'}},
match: '^%([\\w]+)\\b',
name: 'meta.directive.idris'
}
]
},
escape_characters: {
patterns: [
{
match:
'\\\\(NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|SP|DEL|[abfnrtv\\\\\\"\'\\&])',
name: 'constant.character.escape.ascii.idris'
},
{
match: '\\\\o[0-7]+|\\\\x[0-9A-Fa-f]+|\\\\[0-9]+',
name: 'constant.character.escape.octal.idris'
},
{
match: '\\^[A-Z@\\[\\]\\\\\\^_]',
name: 'constant.character.escape.control.idris'
}
]
},
function_signature: {
begin: "(([\\w']+)|\\(([|!%$+\\-.,=</>:]+)\\))\\s*(:)(?!:)",
beginCaptures: {
2: {name: 'entity.name.function.idris'},
3: {name: 'entity.name.function.idris'},
4: {name: 'keyword.operator.colon.idris'}
},
end: '(;|(?<=[^\\s>])\\s*(?!->)\\s*$)',
name: 'meta.function.type-signature.idris',
patterns: [{include: '#type_signature'}]
},
language_const: {
patterns: [
{match: '\\(\\)', name: 'constant.language.unit.idris'},
{match: '_\\|_', name: 'constant.language.bottom.idris'},
{match: '\\b_\\b', name: 'constant.language.underscore.idris'}
]
},
language_keyword: {
patterns: [
{
match: '\\b(infix[lr]?|let|where|of|with)\\b',
name: 'keyword.other.idris'
},
{
match: '\\b(do|if|then|else|case|in)\\b',
name: 'keyword.control.idris'
}
]
},
parameter_type: {
patterns: [
{include: '#prelude_type'},
{
begin: "\\(([\\w']+)\\s*:(?!:)",
beginCaptures: {1: {name: 'entity.name.tag.idris'}},
end: '\\)',
name: 'meta.parameter.named.idris',
patterns: [{include: '#prelude_type'}]
},
{
begin: "\\{((auto|default .+)\\s+)?([\\w']+)\\s*:(?!:)",
beginCaptures: {
1: {name: 'storage.modifier.idris'},
3: {name: 'entity.name.tag.idris'}
},
end: '\\}',
name: 'meta.parameter.implicit.idris',
patterns: [{include: '#prelude_type'}]
}
]
},
prelude: {
patterns: [
{include: '#prelude_class'},
{include: '#prelude_type'},
{include: '#prelude_function'},
{include: '#prelude_const'}
]
},
prelude_class: {
match:
'\\b(Eq|Ord|Num|MinBound|MaxBound|Integral|Applicative|Alternative|Cast|Foldable|Functor|Monad|Traversable|Uninhabited|Semigroup|VerifiedSemigroup|Monoid|VerifiedMonoid|Group|VerifiedGroup|AbelianGroup|VerifiedAbelianGroup|Ring|VerifiedRing|RingWithUnity|VerifiedRingWithUnity|JoinSemilattice|VerifiedJoinSemilattice|MeetSemilattice|VerifiedMeetSemilattice|BoundedJoinSemilattice|VerifiedBoundedJoinSemilattice|BoundedMeetSemilattice|VerifiedBoundedMeetSemilattice|Lattice|VerifiedLattice|BoundedLattice|VerifiedBoundedLattice)\\b',
name: 'support.class.prelude.idris'
},
prelude_const: {
patterns: [
{
match: '\\b(Just|Nothing|Left|Right|True|False|LT|EQ|GT)\\b',
name: 'support.constant.prelude.idris'
}
]
},
prelude_function: {
match:
'\\b(abs|acos|all|and|any|asin|atan|atan2|break|ceiling|compare|concat|concatMap|const|cos|cosh|curry|cycle|div|drop|dropWhile|elem|encodeFloat|enumFrom|enumFromThen|enumFromThenTo|enumFromTo|exp|fail|filter|flip|floor|foldl|foldl1|foldr|foldr1|fromInteger|fst|gcd|getChar|getLine|head|id|init|iterate|last|lcm|length|lines|log|lookup|map|max|maxBound|maximum|maybe|min|minBound|minimum|mod|negate|not|null|or|pi|pred|print|product|putChar|putStr|putStrLn|readFile|recip|repeat|replicate|return|reverse|scanl|scanl1|sequence|sequence_|show|sin|sinh|snd|span|splitAt|sqrt|succ|sum|tail|take|takeWhile|tan|tanh|uncurry|unlines|unwords|unzip|unzip3|words|writeFile|zip|zip3|zipWith|zipWith3)\\b',
name: 'support.function.prelude.idris'
},
prelude_type: {
match:
'\\b(Type|Exists|World|IO|IntTy|FTy|Foreign|File|Mode|Dec|Bool|so|Ordering|Either|Fin|IsJust|List|Maybe|Nat|LTE|GTE|GT|LT|Stream|StrM|Vect|Not|Lazy|Inf|FalseElim)\\b',
name: 'support.type.prelude.idris'
},
type_signature: {
patterns: [
{include: '#context_signature'},
{include: '#parameter_type'},
{include: '#language_const'},
{match: '->', name: 'keyword.operator.arrow.idris'}
]
}
},
scopeName: 'source.idris'
}
export default grammar