X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2FPATTERNS;fp=helm%2FDEVEL%2Fmathml_editor%2FPATTERNS;h=0e5814d82824cb0a45ce3637edf4af090be27329;hp=0000000000000000000000000000000000000000;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hpb=b1fb6b8e1767d775bc452303629e95941d142bea

diff --git a/helm/DEVEL/mathml_editor/PATTERNS b/helm/DEVEL/mathml_editor/PATTERNS
new file mode 100644
index 000000000..0e5814d82
--- /dev/null
+++ b/helm/DEVEL/mathml_editor/PATTERNS
@@ -0,0 +1,196 @@
+
+identifier #
+
+	insert(<mi>#</mi>)
+
+number #
+
+	insert(<mi>#</mi>)
+
+\sqrt
+
+	replace($, <msqrt>$</msqrt>)
+
+\root
+
+	replace($, <mroot><mrow/><mrow>$</mrow></mroot>)
+
+\of
+
+	when (isa($.parent, "mrow") && isa($.parent.parent, "mroot"))
+	let mroot = $.parent.parent
+	if ($.prev and !$.prev.prev and !$.next) replace($.parent, $.prev)
+	replace(mroot.child[0], $)
+
+\underline
+
+	insert(<munder>[$, <mo>&UnderBar;</mo>]</munder>)
+
+\overline
+
+	insert(<mover>[$, <mo>&OverBar;</mo>]</mover>)
+
+\cases
+
+	replace($, <mrow><mo>{</mo><mtable>$</mtable></mrow>)
+
+\matrix
+
+	replace($, <mtable>$</mtable>)
+
+\over
+
+	if isa($.parent, "mrow")
+		replace($.parent, <mfrac>[$.parent, $]</mfrac>)
+
+
+_	if isa($.parent, "mrow")
+		if eq($.prev, null)
+			replace($, new(mmultiscripts, [ new mrow, $, new none ]))
+		elseif (isa($.prev, msub))
+			let base = $.prev.children[0]
+			let script = $.prev.children[1]
+			replace($.rev, new(mmultiscripts, [ base, script, new none, $, new none ]))
+		elseif (isa($.prev, msup))
+			let base = $.prev.children[0]
+			let script = $.prev.children[1]
+			replace($.prev, new(msubsup, [ base, $, script ]))
+		elseif (isa($.prev, msubsup))
+			let base = $.prev.children[0]
+			let subscript = $.prev.children[1]
+			let superscript = $.prev.children[2]
+			replace($.prev, new(mmultiscripts, [ base, subscript, superscript, $, new none ]))
+		elseif isa($.prev, mmultiscripts)
+			if ($.prev.children[$.prev.children.size - 2] = null)
+				replace($.prev.children[$.prev.children.size - 2], $)
+			else
+				$.prev.children.append([$, new none])
+		else
+			replace($.prev, new(msub, [ $.prev, $ ]))
+	else if isa($.parent, msub) and $.parent.children[1] = $
+		let base = $.parent.children[0]
+		replace($.parent, new(munder, [ base, $ ]))
+
+		
+_, \sb (subscript)
+
+	if parent.isa(mrow)
+		if cursor is first child then
+			sub = new mmultiscripts
+			parent.replace(cursor, sub);
+			sub.set_base(new mrow);
+			sub.set_subscript(cursor);
+		else
+			elem = element prior to cursor in parent
+			if elem.isa(msub) || elem.isa(msup) || elem.isa(mmultiscripts) then
+				append script to multiscript and/or replace single script with
+				multiscript
+			else if elem.isa(munder) || elem.isa(mover) || elem.isa(munderover) then
+				creates another munder
+			else
+				parent.replace(elem, sub);
+				sub.set_base(elem);
+				sub.set_subscript(cursor);
+	else if (parent.isa(msub) and cursor is subscript) or
+		change msub into a munder
+		cursor in same position
+	else
+		replace cursor with msub with empty base
+
+^, \sp (superscript)
+
+	symmetric to subscript
+
+', \prime (prime)
+
+	similar to superscript, but multiple prime superscripts should go
+	together in the same operator
+
+{	(group open)
+
+	replace cursor with mrow, put cursor inside mrow
+	if cursor is inside a table, create a new table row and a new table cell
+	and put the cursor inside the cell
+
+}	(group close)
+
+	remove cursor from mrow
+	mrow.parent.advance(cursor, mrow)
+	if cursor inside a table cell then close table
+	
+\over,\atop,\above (fraction)
+
+	if cursor.parent.isa(mrow) then
+		frac = new mfrac
+		cursor.parent.parent.replace(mrow, frac)
+		numerator is current content of cursor.parent except for the cursor
+		itself.
+		set denominator to cursor
+	else
+
+\choose
+
+	similar to fractions, but with stretchable parentheses around
+
+\sqrt
+
+	parent.replace(cursor, new msqrt)
+	set new msqrt.base to cursor
+
+\root
+
+	parent.replace(cursor, new mroot)
+	set empty base element
+	set root index to cursor
+
+\of
+
+	check if cursor.parent is mroot (or mrow inside mroot index)
+	or and cursor is in index position. move the cursor to the base element
+
+\underline
+
+	create munder element with stretchable horizontal line as underscript
+	substitute cursor with munder
+	move the cursor in the base element
+
+\overline
+
+	symmetric
+
+accents (\hat)
+
+	create an mover with accent=true and the operator has stretchy=false
+
+wide accents (\widehat)
+
+	as accents, but mover has accent=false and the operator has stretchy=true
+
+\scriptstyle, ...
+
+	create an appropriate mstyle, the cursor moves in. However, when the
+	subformula ends one has to skip the mstyle
+
+\cases
+
+	create mrow with stretchable brace and emtpy table, put cursor inside
+	table
+
+\matrix
+
+	create empty table, cursor inside table
+
+&
+
+	check that cursor is inside a table cell
+	create a new cell next to it
+
+\cr
+
+	check that cursor is inside a table cell inside a table row
+	create a new row
+
+\phantom
+
+	create a mphantom element, cursor inside
+