progress
This commit is contained in:
tomaz1502
parent
e5a9112e21
commit
3db85481c2
|
|
@ -1,12 +1,54 @@
|
|||
// Reference: https://github.com/leanprover/vscode-lean4
|
||||
// OBS: progress being tracked at ~/Projects/lean-obsi/vscode-lean4/vscode-lean4/syntaxes/lean4.json
|
||||
// TODO: consider operators and numbers in the middle of other strings
|
||||
|
||||
(function (Prism) {
|
||||
Prism.languages.lean = {
|
||||
'string': {
|
||||
pattern: /"(?:[^\\"]|\\(?:\S|\s+\\))*"/,
|
||||
greedy: true
|
||||
// OK
|
||||
'number': [
|
||||
/\b0b[01]+\b/i, // Binary
|
||||
/\b0o[0-7]+\b/i, // Octal
|
||||
/\b0x[0-9a-f]+\b/i, // Hexadecimal
|
||||
/-?[0-9]+\.?[0-9]*(e[-+]?[0-9]+)?\b/i // Regular / Scientific notation
|
||||
],
|
||||
|
||||
// OK
|
||||
'comment': [
|
||||
/\/--[^-\/]*-\//, // Doc comment
|
||||
/\/-![^-\/]*-\//, // Mod doc comment
|
||||
/\/-[^-\/]*-\//, // Block comment
|
||||
// OBS: We left single-line for last to give priority to /-- -/
|
||||
/--.*$/m // Single-line comment
|
||||
],
|
||||
|
||||
'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)\b/,
|
||||
/#(print|eval|reduce|check_failure|check)/
|
||||
],
|
||||
|
||||
// Missing modifiers
|
||||
'function-definition': {
|
||||
pattern: /(\b(?:inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\s+)\w+/,
|
||||
lookbehind: true,
|
||||
alias: 'function'
|
||||
},
|
||||
'number': /\b(?:[-]?\d+(?:\.\d+)?(?:e[+-]?\d+)?|0b[01]+|0o[0-7]+|0x[0-9a-f]+)\b/i,
|
||||
'comment': {
|
||||
pattern: /--.*\r\n/m
|
||||
|
||||
'decorator': {
|
||||
pattern: /@\[[^\]\n]*\]/,
|
||||
alias: ['punctuation']
|
||||
},
|
||||
|
||||
'punctuation' : /[()\[\]{},:]/,
|
||||
|
||||
'operator' : /(\+|\*|-|\/|:=|>>>|<<<|\^\^\^|&&&|\|\|\||\+\+|\^|%|~~~|<|<=|>|>=|==|=)/,
|
||||
|
||||
'boolean' : /\b(true|false)\b/,
|
||||
|
||||
'important': /\b(sorry|admit)\b/,
|
||||
|
||||
// TODO: string interpolation, embedded unicode
|
||||
'string': []
|
||||
|
||||
// TODO: quotation (`)
|
||||
};
|
||||
}(Prism));
|
||||
|
|
@ -0,0 +1 @@
|
|||
!function(e){e.languages.lean={string:{pattern:/"(?:[^\\"]|\\(?:\S|\s+\\))*"/,greedy:!0},number:/\b(?:[-]?\d+(?:\.\d+)?(?:e[+-]?\d+)?|0b[01]+|0o[0-7]+|0x[0-9a-f]+)\b/i,comment:[/--.*$/m,/\/-[^-\/]-\//]}}(Prism);
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
#check Nat
|
||||
#eval 1 + 1
|
||||
#check_failure f
|
||||
#reduce Y
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
[
|
||||
["keyword", "#check"], " Nat\r\n",
|
||||
["keyword", "#eval"], ["number", "1"], ["operator", "+"], ["number", "1"],
|
||||
["keyword", "#check_failure"], " f\r\n",
|
||||
["keyword", "#reduce"], " Y"
|
||||
]
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
Checks tokenization of commands.
|
||||
|
|
@ -1,11 +1,27 @@
|
|||
blah
|
||||
-- foo
|
||||
--
|
||||
/- bar -/
|
||||
/- multi
|
||||
line
|
||||
comment -/
|
||||
/-! Mod doc comment -/
|
||||
-- another single line comment
|
||||
/-- Documentation
|
||||
commentary
|
||||
-/
|
||||
|
||||
---------------------------------------
|
||||
----------------------------------------------------
|
||||
|
||||
[
|
||||
"blah"
|
||||
["comment", "-- foo"],
|
||||
["comment", "--"],
|
||||
["comment", "/- bar -/"],
|
||||
["comment", "/- multi\r\nline\r\ncomment -/"],
|
||||
["comment", "/-! Mod doc comment -/"],
|
||||
["comment", "-- another single line comment"],
|
||||
["comment", "/-- Documentation\r\ncommentary\r\n-/"]
|
||||
]
|
||||
|
||||
---------------------------------------
|
||||
----------------------------------------------------
|
||||
|
||||
tomaz
|
||||
Checks for single-line and documentation comments.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,28 @@
|
|||
@[decorator] def f := 2+2 + 3 - 4 ||| false == true = 3
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
[
|
||||
["decorator", "@[decorator]"],
|
||||
["keyword", "def"],
|
||||
" f ",
|
||||
["punctuation", ":"],
|
||||
["operator", "="],
|
||||
["number", "2"],
|
||||
["operator", "+"],
|
||||
["number", "2"],
|
||||
["operator", "+"],
|
||||
["number", "3"],
|
||||
["operator", "-"],
|
||||
["number", "4"],
|
||||
["operator", "|||"],
|
||||
["boolean", "false"],
|
||||
["operator", "=="],
|
||||
["boolean", "true"],
|
||||
["operator", "="],
|
||||
["number", "3"]
|
||||
]
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
Checks tokenization of decorators.
|
||||
|
|
@ -0,0 +1,39 @@
|
|||
3.14159
|
||||
42
|
||||
3e5
|
||||
-3.14159
|
||||
-42
|
||||
3e-5
|
||||
-3e5
|
||||
-3e-5
|
||||
foo-3e+10bar
|
||||
0b1
|
||||
0B0101
|
||||
0o13
|
||||
0O701
|
||||
0xabcdef
|
||||
0XC0fFEe190
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
[
|
||||
["number", "3.14159"],
|
||||
["number", "42"],
|
||||
["number", "3e5"],
|
||||
["number", "-3.14159"],
|
||||
["number", "-42"],
|
||||
["number", "3e-5"],
|
||||
["number", "-3e5"],
|
||||
["number", "-3e-5"],
|
||||
"\r\ntomaz", ["operator", "-"], "3e", ["operator", "+"], "10gomes\r\n",
|
||||
["number", "0b1"],
|
||||
["number", "0B0101"],
|
||||
["number", "0o13"],
|
||||
["number", "0O701"],
|
||||
["number", "0xabcdef"],
|
||||
["number", "0XC0fFEe190"]
|
||||
]
|
||||
|
||||
----------------------------------------------------
|
||||
|
||||
Checks tokenization of numbers (binary, octal, hexadecimal, scientific notation).
|
||||
Loading…
Reference in New Issue