]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/PATTERNS
Initial revision
[helm.git] / helm / DEVEL / mathml_editor / PATTERNS
diff --git a/helm/DEVEL/mathml_editor/PATTERNS b/helm/DEVEL/mathml_editor/PATTERNS
new file mode 100644 (file)
index 0000000..0e5814d
--- /dev/null
@@ -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
+