Merge pull request #619 from Golmote/prism-mizar

Add support for Mizar

components.js

@@ -250,6 +250,10 @@ var components = {
 			"title": "MEL",
 			"owner": "Golmote"
 		},
+		"mizar": {
+			"title": "Mizar",
+			"owner": "Golmote"
+		},
 		"nasm": {
 			"title": "NASM",
 			"owner": "rbmj"

components/prism-mizar.js

@@ -0,0 +1,12 @@
+Prism.languages.mizar = {
+	'comment': /::.+/,
+	'keyword': /@proof\b|\b(?:according|aggregate|all|and|antonym|are|as|associativity|assume|asymmetry|attr|be|begin|being|by|canceled|case|cases|clusters?|coherence|commutativity|compatibility|connectedness|consider|consistency|constructors|contradiction|correctness|def|deffunc|define|definitions?|defpred|do|does|equals|end|environ|ex|exactly|existence|for|from|func|given|hence|hereby|holds|idempotence|identity|iff?|implies|involutiveness|irreflexivity|is|it|let|means|mode|non|not|notations?|now|of|or|otherwise|over|per|pred|prefix|projectivity|proof|provided|qua|reconsider|redefine|reduce|reducibility|reflexivity|registrations?|requirements|reserve|sch|schemes?|section|selector|set|sethood|st|struct|such|suppose|symmetry|synonym|take|that|the|then|theorems?|thesis|thus|to|transitivity|uniqueness|vocabular(?:y|ies)|when|where|with|wrt)\b/,
+	'parameter': {
+		pattern: /\$(?:10|\d)/,
+		alias: 'variable'
+	},
+	'variable': /\w+(?=:)/,
+	'number': /(?:\b|-)\d+\b/,
+	'operator': /\.\.\.|->|&|\.?=/,
+	'punctuation': /\(#|#\)|[,:;\[\](){}]/
+};

examples/prism-mizar.html

@@ -0,0 +1,48 @@
+<h1>Mizar</h1>
+<p>To use this language, use the class "language-mizar".</p>
+
+<h2>Full example</h2>
+
+<pre><code>:: Example from http://webdocs.cs.ualberta.ca/~piotr/Mizar/Dagstuhl97/
+environ
+vocabulary SCM;
+constructors ARYTHM, PRE_FF, NAT_1, REAL_1;
+notation ARYTHM, PRE_FF, NAT_1;
+requirements ARYTHM;
+theorems REAL_1, PRE_FF, NAT_1, AXIOMS, CQC_THE1;
+schemes NAT_1;
+begin
+
+P: for k being Nat
+	st for n being Nat st n < k holds Fib (n+1) ≥ n
+		holds Fib (k+1) ≥ k
+proof let k be Nat; assume
+IH: for n being Nat st n < k holds Fib (n+1) ≥ n;
+	per cases;
+		suppose k ≤ 1; then k = 0 or k = 0+1 by CQC_THE1:2;
+			hence Fib (k+1) ≥ k by PRE_FF:1;
+		suppose 1 < k; then
+			1+1 ≤ k by NAT_1:38; then
+			consider m being Nat such that
+		A: k = 1+1+m by NAT_1:28;
+			thus Fib (k+1) ≥ k proof
+				per cases by NAT_1:19;
+				suppose S1: m = 0;
+					Fib (0+1+1+1) = Fib(0+1) + Fib(0+1+1) by PRE_FF:1
+					              = 1 + 1 by PRE_FF:1;
+					hence Fib (k+1) ≥ k by A, S1;
+				suppose m > 0; then
+					m+1 > 0+1 by REAL_1:59; then
+					m ≥ 1 by NAT_1:38; then
+				B: m+(m+1) ≥ m+1+1 by REAL_1:49;
+				C: k = m+1+1 by A, AXIOMS:13;
+				   m < m+1 & m+1 < m+1+1 by REAL_1:69; then
+				   m < k & m+1 < k by C, AXIOMS:22; then
+				D: Fib (m+1) ≥ m & Fib (m+1+1) ≥ m+1 by IH;
+				   Fib (m+1+1+1) = Fib (m+1) + Fib (m+1+1) by PRE_FF:1; then
+				   Fib (m+1+1+1) ≥ m+(m+1) by D, REAL_1:55;
+		hence Fib(k+1) ≥ k by C, B, AXIOMS:22;
+	end;
+end;
+
+for n being Nat holds Fib(n+1) ≥ n from Comp_Ind(P);</code></pre>

tests/languages/mizar/comment_feature.test

@@ -0,0 +1,11 @@
+:: Foobar
+
+----------------------------------------------------
+
+[
+	["comment", ":: Foobar"]
+]
+
+----------------------------------------------------
+
+Checks for comments.

tests/languages/mizar/keyword_feature.test

@@ -0,0 +1,245 @@
+@proof
+according
+aggregate
+all
+and
+antonym
+are
+as
+associativity
+assume
+asymmetry
+attr
+be
+begin
+being
+by
+canceled
+case
+cases
+cluster
+clusters
+coherence
+commutativity
+compatibility
+connectedness
+consider
+consistency
+constructors
+contradiction
+correctness
+def
+deffunc
+define
+definition
+definitions
+defpred
+do
+does
+equals
+end
+environ
+ex
+exactly
+existence
+for
+from
+func
+given
+hence
+hereby
+holds
+idempotence
+identity
+if
+iff
+implies
+involutiveness
+irreflexivity
+is
+it
+let
+means
+mode
+non
+not
+notation
+notations
+now
+of
+or
+otherwise
+over
+per
+pred
+prefix
+projectivity
+proof
+provided
+qua
+reconsider
+redefine
+reduce
+reducibility
+reflexivity
+registration
+registrations
+requirements
+reserve
+sch
+scheme
+schemes
+section
+selector
+set
+sethood
+st
+struct
+such
+suppose
+symmetry
+synonym
+take
+that
+the
+then
+theorem
+theorems
+thesis
+thus
+to
+transitivity
+uniqueness
+vocabulary
+vocabularies
+when
+where
+with
+wrt
+
+----------------------------------------------------
+
+[
+	["keyword", "@proof"],
+	["keyword", "according"],
+	["keyword", "aggregate"],
+	["keyword", "all"],
+	["keyword", "and"],
+	["keyword", "antonym"],
+	["keyword", "are"],
+	["keyword", "as"],
+	["keyword", "associativity"],
+	["keyword", "assume"],
+	["keyword", "asymmetry"],
+	["keyword", "attr"],
+	["keyword", "be"],
+	["keyword", "begin"],
+	["keyword", "being"],
+	["keyword", "by"],
+	["keyword", "canceled"],
+	["keyword", "case"],
+	["keyword", "cases"],
+	["keyword", "cluster"],
+	["keyword", "clusters"],
+	["keyword", "coherence"],
+	["keyword", "commutativity"],
+	["keyword", "compatibility"],
+	["keyword", "connectedness"],
+	["keyword", "consider"],
+	["keyword", "consistency"],
+	["keyword", "constructors"],
+	["keyword", "contradiction"],
+	["keyword", "correctness"],
+	["keyword", "def"],
+	["keyword", "deffunc"],
+	["keyword", "define"],
+	["keyword", "definition"],
+	["keyword", "definitions"],
+	["keyword", "defpred"],
+	["keyword", "do"],
+	["keyword", "does"],
+	["keyword", "equals"],
+	["keyword", "end"],
+	["keyword", "environ"],
+	["keyword", "ex"],
+	["keyword", "exactly"],
+	["keyword", "existence"],
+	["keyword", "for"],
+	["keyword", "from"],
+	["keyword", "func"],
+	["keyword", "given"],
+	["keyword", "hence"],
+	["keyword", "hereby"],
+	["keyword", "holds"],
+	["keyword", "idempotence"],
+	["keyword", "identity"],
+	["keyword", "if"],
+	["keyword", "iff"],
+	["keyword", "implies"],
+	["keyword", "involutiveness"],
+	["keyword", "irreflexivity"],
+	["keyword", "is"],
+	["keyword", "it"],
+	["keyword", "let"],
+	["keyword", "means"],
+	["keyword", "mode"],
+	["keyword", "non"],
+	["keyword", "not"],
+	["keyword", "notation"],
+	["keyword", "notations"],
+	["keyword", "now"],
+	["keyword", "of"],
+	["keyword", "or"],
+	["keyword", "otherwise"],
+	["keyword", "over"],
+	["keyword", "per"],
+	["keyword", "pred"],
+	["keyword", "prefix"],
+	["keyword", "projectivity"],
+	["keyword", "proof"],
+	["keyword", "provided"],
+	["keyword", "qua"],
+	["keyword", "reconsider"],
+	["keyword", "redefine"],
+	["keyword", "reduce"],
+	["keyword", "reducibility"],
+	["keyword", "reflexivity"],
+	["keyword", "registration"],
+	["keyword", "registrations"],
+	["keyword", "requirements"],
+	["keyword", "reserve"],
+	["keyword", "sch"],
+	["keyword", "scheme"],
+	["keyword", "schemes"],
+	["keyword", "section"],
+	["keyword", "selector"],
+	["keyword", "set"],
+	["keyword", "sethood"],
+	["keyword", "st"],
+	["keyword", "struct"],
+	["keyword", "such"],
+	["keyword", "suppose"],
+	["keyword", "symmetry"],
+	["keyword", "synonym"],
+	["keyword", "take"],
+	["keyword", "that"],
+	["keyword", "the"],
+	["keyword", "then"],
+	["keyword", "theorem"],
+	["keyword", "theorems"],
+	["keyword", "thesis"],
+	["keyword", "thus"],
+	["keyword", "to"],
+	["keyword", "transitivity"],
+	["keyword", "uniqueness"],
+	["keyword", "vocabulary"],
+	["keyword", "vocabularies"],
+	["keyword", "when"],
+	["keyword", "where"],
+	["keyword", "with"],
+	["keyword", "wrt"]
+]
+
+----------------------------------------------------
+
+Checks for keywords.

tests/languages/mizar/number_feature.test

@@ -0,0 +1,15 @@
+0
+-2
+42
+
+----------------------------------------------------
+
+[
+	["number", "0"],
+	["number", "-2"],
+	["number", "42"]
+]
+
+----------------------------------------------------
+
+Checks for numbers.

tests/languages/mizar/operator_feature.test

@@ -0,0 +1,17 @@
+...
+->
+&
+= .=
+
+----------------------------------------------------
+
+[
+	["operator", "..."],
+	["operator", "->"],
+	["operator", "&"],
+	["operator", "="], ["operator", ".="]
+]
+
+----------------------------------------------------
+
+Checks for operators.

tests/languages/mizar/parameter_feature.test

@@ -0,0 +1,17 @@
+$1 $2 $3
+$4 $5 $6
+$6 $7 $9
+$10
+
+----------------------------------------------------
+
+[
+	["parameter", "$1"], ["parameter", "$2"], ["parameter", "$3"],
+	["parameter", "$4"], ["parameter", "$5"], ["parameter", "$6"],
+	["parameter", "$6"], ["parameter", "$7"], ["parameter", "$9"],
+	["parameter", "$10"]
+]
+
+----------------------------------------------------
+
+Checks for parameters.