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

diff --git a/helm/DEVEL/mathml_editor/PATTERNS b/helm/DEVEL/mathml_editor/PATTERNS
deleted file mode 100644
index 0e5814d82..000000000
--- a/helm/DEVEL/mathml_editor/PATTERNS
+++ /dev/null
@@ -1,196 +0,0 @@
-
-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
-