]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/mathml_editor/PATTERNS
added annotations to Cic.Implicit
[helm.git] / helm / DEVEL / mathml_editor / PATTERNS
1
2 identifier #
3
4         insert(<mi>#</mi>)
5
6 number #
7
8         insert(<mi>#</mi>)
9
10 \sqrt
11
12         replace($, <msqrt>$</msqrt>)
13
14 \root
15
16         replace($, <mroot><mrow/><mrow>$</mrow></mroot>)
17
18 \of
19
20         when (isa($.parent, "mrow") && isa($.parent.parent, "mroot"))
21         let mroot = $.parent.parent
22         if ($.prev and !$.prev.prev and !$.next) replace($.parent, $.prev)
23         replace(mroot.child[0], $)
24
25 \underline
26
27         insert(<munder>[$, <mo>&UnderBar;</mo>]</munder>)
28
29 \overline
30
31         insert(<mover>[$, <mo>&OverBar;</mo>]</mover>)
32
33 \cases
34
35         replace($, <mrow><mo>{</mo><mtable>$</mtable></mrow>)
36
37 \matrix
38
39         replace($, <mtable>$</mtable>)
40
41 \over
42
43         if isa($.parent, "mrow")
44                 replace($.parent, <mfrac>[$.parent, $]</mfrac>)
45
46
47 _       if isa($.parent, "mrow")
48                 if eq($.prev, null)
49                         replace($, new(mmultiscripts, [ new mrow, $, new none ]))
50                 elseif (isa($.prev, msub))
51                         let base = $.prev.children[0]
52                         let script = $.prev.children[1]
53                         replace($.rev, new(mmultiscripts, [ base, script, new none, $, new none ]))
54                 elseif (isa($.prev, msup))
55                         let base = $.prev.children[0]
56                         let script = $.prev.children[1]
57                         replace($.prev, new(msubsup, [ base, $, script ]))
58                 elseif (isa($.prev, msubsup))
59                         let base = $.prev.children[0]
60                         let subscript = $.prev.children[1]
61                         let superscript = $.prev.children[2]
62                         replace($.prev, new(mmultiscripts, [ base, subscript, superscript, $, new none ]))
63                 elseif isa($.prev, mmultiscripts)
64                         if ($.prev.children[$.prev.children.size - 2] = null)
65                                 replace($.prev.children[$.prev.children.size - 2], $)
66                         else
67                                 $.prev.children.append([$, new none])
68                 else
69                         replace($.prev, new(msub, [ $.prev, $ ]))
70         else if isa($.parent, msub) and $.parent.children[1] = $
71                 let base = $.parent.children[0]
72                 replace($.parent, new(munder, [ base, $ ]))
73
74                 
75 _, \sb (subscript)
76
77         if parent.isa(mrow)
78                 if cursor is first child then
79                         sub = new mmultiscripts
80                         parent.replace(cursor, sub);
81                         sub.set_base(new mrow);
82                         sub.set_subscript(cursor);
83                 else
84                         elem = element prior to cursor in parent
85                         if elem.isa(msub) || elem.isa(msup) || elem.isa(mmultiscripts) then
86                                 append script to multiscript and/or replace single script with
87                                 multiscript
88                         else if elem.isa(munder) || elem.isa(mover) || elem.isa(munderover) then
89                                 creates another munder
90                         else
91                                 parent.replace(elem, sub);
92                                 sub.set_base(elem);
93                                 sub.set_subscript(cursor);
94         else if (parent.isa(msub) and cursor is subscript) or
95                 change msub into a munder
96                 cursor in same position
97         else
98                 replace cursor with msub with empty base
99
100 ^, \sp (superscript)
101
102         symmetric to subscript
103
104 ', \prime (prime)
105
106         similar to superscript, but multiple prime superscripts should go
107         together in the same operator
108
109 {       (group open)
110
111         replace cursor with mrow, put cursor inside mrow
112         if cursor is inside a table, create a new table row and a new table cell
113         and put the cursor inside the cell
114
115 }       (group close)
116
117         remove cursor from mrow
118         mrow.parent.advance(cursor, mrow)
119         if cursor inside a table cell then close table
120         
121 \over,\atop,\above (fraction)
122
123         if cursor.parent.isa(mrow) then
124                 frac = new mfrac
125                 cursor.parent.parent.replace(mrow, frac)
126                 numerator is current content of cursor.parent except for the cursor
127                 itself.
128                 set denominator to cursor
129         else
130
131 \choose
132
133         similar to fractions, but with stretchable parentheses around
134
135 \sqrt
136
137         parent.replace(cursor, new msqrt)
138         set new msqrt.base to cursor
139
140 \root
141
142         parent.replace(cursor, new mroot)
143         set empty base element
144         set root index to cursor
145
146 \of
147
148         check if cursor.parent is mroot (or mrow inside mroot index)
149         or and cursor is in index position. move the cursor to the base element
150
151 \underline
152
153         create munder element with stretchable horizontal line as underscript
154         substitute cursor with munder
155         move the cursor in the base element
156
157 \overline
158
159         symmetric
160
161 accents (\hat)
162
163         create an mover with accent=true and the operator has stretchy=false
164
165 wide accents (\widehat)
166
167         as accents, but mover has accent=false and the operator has stretchy=true
168
169 \scriptstyle, ...
170
171         create an appropriate mstyle, the cursor moves in. However, when the
172         subformula ends one has to skip the mstyle
173
174 \cases
175
176         create mrow with stretchable brace and emtpy table, put cursor inside
177         table
178
179 \matrix
180
181         create empty table, cursor inside table
182
183 &
184
185         check that cursor is inside a table cell
186         create a new cell next to it
187
188 \cr
189
190         check that cursor is inside a table cell inside a table row
191         create a new row
192
193 \phantom
194
195         create a mphantom element, cursor inside
196