Add Lean support

components.json

@@ -840,6 +840,10 @@
 			"require": ["clike", "markup-templating", "php"],
 			"owner": "nette"
 		},
+		"lean": {
+			"title": "Lean",
+			"owner": "tomaz1502"
+		},
 		"less": {
 			"title": "Less",
 			"require": "css",
@@ -1763,4 +1767,4 @@
 			"owner": "Golmote"
 		}
 	}
-}
+}

components/prism-lean.js

@@ -0,0 +1,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));

examples/prism-lean.html

@@ -0,0 +1,60 @@
+<h2>Comments</h2>
+<pre><code>
+-- foo
+--
+/- bar -/
+/- multi
+line
+comment -/
+/-! Mod doc comment -/
+-- another single line comment
+/-- Documentation
+commentary
+-/
+</code></pre>
+
+<h2>Strings</h2>
+<pre><code>
+"foo
+bar
+baz"
+'foo bar baz'
+</pre></code>
+
+<h2>Numbers</h2>
+<pre><code>
+foo314bar
+3.14159
+42
+3e5
+-3.14159
+-42
+3e-5
+-3e5
+-3e-5
+0b1
+0B0101
+0o13
+0O701
+0xabcdef
+0XC0fFEe190
+</code></pre>
+
+<h2>Full example</h2>
+<pre><code>
+partial def String.isSubStrOf (sub : String) (s : String) : Bool :=
+  loop 0
+  where
+    loop i :=
+	  if i + sub.length > s.length then false
+	  else String.substrEq sub 0 s ⟨i⟩ sub.length \/ loop (i + 1)
+
+/-- (Extracted from prelude)
+The notation typeclass for heterogeneous append.
+This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
+-/
+class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  /-- `a ++ b` is the result of concatenation of `a` and `b`, usually read "append".
+  The meaning of this notation is type-dependent. -/
+  hAppend : α → β → γ
+</code></pre>

tests/languages/lean/commands_feature.test

@@ -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.

tests/languages/lean/comment_feature.test

@@ -0,0 +1,27 @@
+-- foo
+--
+/- bar -/
+/- multi
+line
+comment-/
+/-! Mod doc comment -/
+-- another single line comment
+/-- Documentati q23 # ( *) @ on
+com-mentary
+-/
+
+----------------------------------------------------
+
+[
+	["comment", "-- foo"],
+	["comment", "--"],
+	["comment", "/- bar -/"],
+	["comment", "/- multi\r\nline\r\ncomment-/"],
+	["comment", "/-! Mod doc comment -/"],
+	["comment", "-- another single line comment"],
+	["comment", "/-- Documentati q23 # ( *) @ on\r\ncom-mentary\r\n-/"]
+]
+
+----------------------------------------------------
+
+Checks for single-line and documentation comments.

tests/languages/lean/decorator_feature.test

@@ -0,0 +1,28 @@
+@[decorator foo.bar] def f := 2+2 + 3 - 4 ||| false == true = 3
+
+----------------------------------------------------
+
+[
+	["decorator", "@[decorator foo.bar]"],
+	["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.

tests/languages/lean/numbers_feature.test

@@ -0,0 +1,39 @@
+foo314bar
+3.14159
+42
+3e5
+-3.14159
+-42
+3e-5
+-3e5
+-3e-5
+0b1
+0B0101
+0o13
+0O701
+0xabcdef
+0XC0fFEe190
+
+----------------------------------------------------
+
+[
+	"foo314bar\r\n",
+	["number", "3.14159"],
+	["number", "42"],
+	["number", "3e5"],
+	["number", "-3.14159"],
+	["number", "-42"],
+	["number", "3e-5"],
+	["number", "-3e5"],
+	["number", "-3e-5"],
+	["number", "0b1"],
+	["number", "0B0101"],
+	["number", "0o13"],
+	["number", "0O701"],
+	["number", "0xabcdef"],
+	["number", "0XC0fFEe190"]
+]
+
+----------------------------------------------------
+
+Checks tokenization of numbers (binary, octal, hexadecimal, scientific notation).

tests/languages/lean/quotation_feature.test

@@ -0,0 +1,12 @@
+`Foo.bar.baz bam
+`Foobar
+
+----------------------------------------------------
+[
+	["quotation", "`Foo.bar.baz"],
+	" bam\r\n",
+	["quotation", "`Foobar"]
+]
+----------------------------------------------------
+
+Checks tokenization of quotations (`)

tests/languages/lean/string_feature.test

@@ -0,0 +1,15 @@
+"foo
+bar
+baz"
+'foo bar baz'
+
+----------------------------------------------------
+
+[
+	["string", "\"foo\r\nbar\r\nbaz\""],
+	["string", "'foo bar baz'"]
+]
+
+----------------------------------------------------
+
+Test tokenization of strings.