]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/PATTERNS
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / DEVEL / mathml_editor / PATTERNS
diff --git a/helm/DEVEL/mathml_editor/PATTERNS b/helm/DEVEL/mathml_editor/PATTERNS
deleted file mode 100644 (file)
index 0e5814d..0000000
+++ /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
-