From: Paolo Marinelli Date: Mon, 31 Mar 2003 15:35:17 +0000 (+0000) Subject: Added epsilon-rules concerning the left drop. X-Git-Tag: before_refactoring~75 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef1b1369e26bdae74fb721abe4cd51c954ef48f6;p=helm.git Added epsilon-rules concerning the left drop. --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 55e17218a..ed95dcf14 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -523,32 +523,8 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \begin{description} - %******************************************************************************************************* - %************** rules handling the case in which the cursor has a preceding node *********************** - %******************************************************************************************************* - - %************** cursor's parent is a group or a parameter (a p node) - - \item{\verb+[(i|n|o|s|c[!*])#]/cursor+}\\ - remove the token. - - \item{\verb+[g#]/cursor+}\\ - remove the cursor and append it to the \G{} node. - - \item{\verb+[#]cursor+}\\ - remove the cursor and append the $\SLDSCRIPT$ - - \item{\verb+[c[p[@right-open="1"]$]#]/cursor+}\\ - remove the cursor and append the it to the \PNODE{} node. - - % remember to add the rules handling the primes - - %************************************************************************************************* - %*********** rules handling the case in which the cursor has no preceding nodes ****************** - %************************************************************************************************* - - \item{\verb+g[@id][^#$]/cursor+}\\ - replace the \G{} node with the cursor. + \item{\verb+cursor+}\\ + replace the cursor with the $\SLDROP$. \end{description} @@ -564,7 +540,7 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node %****************************** epsilon-rules with \NLDROP **************************** %************************************************************************************** - %***************************** \NLDROP has no preceding nodes ************************* + %************** \NLDROP has neither preceding nor following nodes ******************** \item{\verb+math[^#$]/+$\NLDROP$}\\ replace the $\NLDROP$ with the cursor. @@ -572,19 +548,14 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \item{\verb+g[^#$]/+$\NLDROP$}\\ replace the \G{} node with the $\NLDROP$. - % this rule overrides the rule above + % this rule overrides the one above \item{\verb+math/g[^#$]/+$\NLDROP$}\\ replace the $\NLDROP$ with the cursor. + % this rule is overridden by the two ones below \item{\verb+c/p[^#$]/+$\NLDROP$}\\ remove the $\NLDROP$ and insert it before the \PNODE{} node. - \item{\verb+cell[^#$]/+$\NLDROP$}\\ - replace the cell with the $\NLDROP_n$. - - \item{\verb+table[^#$]/+$\NLDROP$}\\ - replace the \TABLE{} node with the $\NLDROP$. - \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\ replace the \CNODE{} node with the content of the first \PNODE{} node and insert the $\NLDROP$ after this content @@ -594,6 +565,12 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \item{\verb+c[^#][!p(*)]/+$\NLDROP$}\\ replace the \CNODE{} node with the $\NLDROP$. + \item{\verb+cell[^#$]/+$\NLDROP$}\\ + replace the cell with the $\NLDROP_n$. + + \item{\verb+table[^#$]/+$\NLDROP$}\\ + replace the \TABLE{} node with the $\NLDROP$. + %************************* \NLDROP has at least one preceding node ********************* % general rules @@ -603,7 +580,7 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node remove the $\NLDROP$ and append it as the last child of its ex preceding brother. % this rule overrides the one above - \item{\verb+*[#]/+$\NLDROP$}\\ + \item{\verb+*[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\ remove the $\NLDROP$ and replace the token with the $\NLDROP_n$. % special rules @@ -644,6 +621,104 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \item{\verb+c[^#][p[*]]/+$\NLDROP$}\\ remove the $\NLDROP$ and insert it before the \CNODE{} node. +\end{description} + +\paragraph{Special Left Drop} + +\begin{description} + + %******************************************************************************************************** + %************************************ epsilon-rules with \SLDROP **************************************** + %******************************************************************************************************** + + \item{\verb+math/+$\SLDROP$}\\ + replace the $\SLDROP$ with the cursor. + + %************************ \SLDROP has neither preceding nor following nodes ***************************** + + % this rule overrides the one below + \item{\verb+math/g[^#$]/+$\SLDROP$}\\ + replace the $\SLDROP$ with the cursor. + + \item{\verb+g[^#$]/+$\SLDROP$}\\ + replace the \G{} node with the cursor. + + \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\ + replace the \CNODE{} node with the content of the first \PNODE{} node and insert the cursor after this content + + \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\ + replace the \CNODE{} node with the cursor. + + \item{\verb+c/p[^#$]/+$\SLDROP$}\\ + remove the $\SLDROP$ and insert it before the \PNODE{} node. + + \item{\verb+c[^#][!p(*)]/+$\SLDROP$}\\ + replace the \CNODE{} node with the cursor. + + \item{\verb+cell[^#$]/+$\SLDROP$}\\ + replace the cell with the $\NLDROP_n$. + + \item{\verb+table[^#$]/+$\SLDROP$}\\ + replace the \TABLE{} node with the cursor. + + %*********************** \SLDROP has at least one preceding node *********************************** + + \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\SLDROP$}\\ + remove the last \ONODE{} node and replace the $\SLDROP$ with the cursor. + + \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\SLDROP$}\\ + replace the script with its first child and replace the $\SLDROP$ with the cursor.%$\NLDROP_n$. + + \item{\verb+[^g[!@id][!*]#$]/+$\SLDROP$}\\ + replace the script with the cursor. + + % this rule is overridden by the three rules above. + \item{\verb+[^*#$]+/$\SLDROP$}\\ + replace the script node with its first child and insert the cursor after it. + + \item{\verb+c[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\ + remove the $\SLDROP$ and insert the cursor before the delimiter. + + \item{\verb+c[p#(i|n|o|s|c[!*])]/+$\SLDROP$}\\ + remove the $\SLDROP$ and insert the cursor into the \PNODE{} node. + + \item{\verb+c[p[@right-open='1']#]+}\\ + remove the $\SLDROP$ and append the curor as last child of the \PNODE{} node. + + % this rule is overridden by the two ones above. + \item{\verb+c[p#]/+$\SLDROP$}\\ + move the $\SLDROP$ into the \PNODE{} node. + + \item{\verb+*[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\ + remove the $\SLDROP$ and replace the token with the cursor. + + \item{\verb+*[table#]/$\SLDROP$+}\\ + remove the $\SLDROP$ and append the $\NLDROP_n$ as the last child of the \TABLE{} node. + + \item{\verb+*[c#]/+$\SLDROP$}\\ + move the $\SLDROP$ into the \CNODE{} node. + + \item{\verb+*[g#]/+$\SLDROP$}\\ + remove the $\SLDROP$ and append the cursor as the last child of the \G{} node. + + %********** \SLDROP has no preceding node, but has following ones ************** + + \item{\verb+math/g[^#*]/+$\SLDROP$}\\ + replace the $\SLDROP$ with the cursor. + + \item{\verb+c[^#p][p(*)]/+$\SLDROP$}\\ + remove the $\SLDROP$ and insert the cursor before the \CNODE{} node. + + % general rule + \item{\verb+*[^#*]/+$\SLDROP$}\\ + remove the $\SLDROP$ and insert the cursor before its parent. + +\end{description} + +\paragraph{Normalize Left Drop} + +\begin{description} + %**************************************************************************************** %***************************** epsilon-rules with \NLDROP_n ***************************** %**************************************************************************************** @@ -661,19 +736,13 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node remove the $\NLDROP_n$ and append it as last child of the \ROW{} node. \item{\verb+table[^#$]/+$\NLDROP_n$}\\ - replace the \texttt{table} with the cursor.%$\NLDROP_n$. + replace the \TABLE{} with the cursor.%$\NLDROP_n$. \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\ replace the \G{} node with the $\NLDROP_n$. \end{description} -\paragraph{Special Left Drop} - -%\begin{description} - -%\end{description} - \paragraph{Advance} \begin{description}