-
Notifications
You must be signed in to change notification settings - Fork 1.3k
/
prism-lean.js
55 lines (44 loc) · 1.71 KB
/
prism-lean.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
// Reference: https://github.com/leanprover/vscode-lean4
// TODO: String interpolation
(function (Prism) {
Prism.languages.lean = {
// OK
'number': [
/\b0b[01]+\b/i, // Binary
/\b0o[0-7]+\b/i, // Octal
/\b0x[0-9a-f]+\b/i, // Hexadecimal
{ pattern: /(\W)-?\d+(?:\.\d+)?(?:e[-+]?\d+)?\b/i,
lookbehind: true
} // Regular / Scientific notation }
],
// OK
'comment': {
pattern: /(?:\/--[\s\S]*?-\/)|(?:\/-![\s\S]*?-\/)|(?:\/-[\s\S]*?-\/)|--.*$/m,
},
'keyword': [
/\b(?:theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break|global|local|scoped|partial|unsafe|private|protected|noncomputable)\b/,
/#(?:print|eval|reduce|check_failure|check)/
],
'function-definition': {
pattern: /(\b(?:inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\s+)\w+/,
lookbehind: true,
alias: 'function'
},
'decorator': {
pattern: /@\[[^\]\n]*\]/,
alias: 'keyword'
},
'punctuation' : /[()\[\]{},:]/,
'operator' : /\+|\*|-|\/|:=|>>>|<<<|\^\^\^|&&&|\|\|\||\+\+|\^|%|~~~|<|<=|>|>=|==|=/,
'boolean' : /\b(?:true|false)\b/,
'important': /\b(?:sorry|admit)\b/,
'string': [
/"[^"]*"/,
/'[^']'/
],
'quotation': {
pattern: /`[^(\s]*/, // Remove `(` to avoid capturing parsers
alias: 'symbol'
}
};
}(Prism));