From: Paolo Marinelli Date: Sat, 29 Mar 2003 20:43:35 +0000 (+0000) Subject: Removed many rules in the "Left Drop" section. Every epsilon-rule in the X-Git-Tag: before_refactoring~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28edc4349551681f63c8491eb09b163b5dedd875;p=helm.git Removed many rules in the "Left Drop" section. Every epsilon-rule in the normal left drop paragraph has been changed. --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 1a99fdbd0..3e3964272 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -26,11 +26,13 @@ \newcommand{\CELL}{\texttt{cell}} \newcommand{\ROW}{\texttt{row}} \newcommand{\SLDROP}{\blacktriangleleft} +\newcommand{\SLDSCRIPT}{\blacktriangleleft_{s}} \newcommand{\NLDROP}{\vartriangleleft} \newcommand{\RGROUP}{\vartriangleleft_{rg}} \newcommand{\NLDGP}{\vartriangleleft_{g}} \newcommand{\NLDSCRIPT}{\vartriangleleft_{s}} -\newcommand{\NLDMACRO}{\vartriangleleft_{c}} % at the moment it's not used. +\newcommand{\NLDMACRO}{\vartriangleleft_{c}} +\newcommand{\NLDTABLE}{\vartriangleleft_{t}} \begin{document} @@ -410,105 +412,135 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \begin{description} - % in the rules below, a token is either an i node, an n node, an o node, an s node or an empty c node. - % an empty c node is either an undefined macro or an empty macro. These c node are handled as they actually were - % tokens (i, n, o, s). - % An important observation is: a sequence of groups with id, in which every group has one and only one child and where - % the last group contains the cursor, is equivalent to the cursor (Is it clear?). For example: - % ...... is equivalent to: - % + \item{\verb+cursor+}\\ + replace the cursor with the $\NLDROP$. - %************************************************************************************************************ - %************************** there is at least one node preceding the cursor ********************************* - %************************************************************************************************************ +\end{description} - %************************** cursor's parent is a group or a parameter (p node). +\paragraph{Special Left Drop:} $\SLDROP$ - \item{\verb+[(i|n|o|s|c[!*])#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and replace the token with the cursor. - - \item{\verb+g[@id][(i|n|o|s|c[!*])#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and replace the token with the $\RGROUP$. +\begin{description} - \item{\verb+[g#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append $\NLDGP$ to the \G{} node preceding the cursor. + %******************************************************************************************************* + %************** rules handling the case in which the cursor has a preceding node *********************** + %******************************************************************************************************* - \item{\verb+[#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDSCRIPT$ to script node. + %************** cursor's parent is a group or a parameter (a p node) - \item{\verb+[c[p[@right-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and apeend the $\NLDGP$ to the \PNODE{} node. + \item{\verb+[(i|n|o|s|c[!*])#]/cursor+}\\ + remove the token. - % we don't have this kind of macro - %\item{\verb+[c[^p[@left-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ + \item{\verb+[g#]/cursor+}\\ + remove the cursor and append it to the \G{} node. - \item{\verb+[c[p[!@left-open="1"][!@right-open="1"](c[!*]|i|n|o|s)*$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDGP$ to the \PNODE{} node. + \item{\verb+[#]cursor+}\\ + remove the cursor and append the $\SLDSCRIPT$ - \item{\verb+*[sp[^*g[!@id][^o[@name="prime"]$]]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - replace (if present) the sequence of \G{} nodes with attribute \texttt{id} with the cursor and replace the \SP{} node with its first child. + \item{\verb+[c[p[@right-open="1"]$]#]/cursor+}\\ + remove the cursor and append the it to the \PNODE{} node. - \item{\verb+*[sp[^*g[!@id][^o[@name="prime"]++\verb+o[@name="prime"]$]]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - replace (if present) the sequence of \G{} nodes with attribute \texttt{id} with the cursor and remove the last \ONODE{}, which is \G{} node's child. + % remember to add the rules handling the primes - %************************************ cursor's parent is a script + %************************************************************************************************* + %*********** rules handling the case in which the cursor has no preceding nodes ****************** + %************************************************************************************************* - \item{\verb+/[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove replace the script with the cursor. + \item{\verb+g[@id][^#$]/cursor+}\\ + replace the \G{} node with the cursor. - \item{\verb+g[@id]/[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - replace the script with the $\RGROUP$. +\end{description} - \item{\verb+[g#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - repalce the script with it's first child (the \G{} node) and append the $\NLDGP$ to it. +\section{Right Drop Rules} - \item{\verb+[^c[p[@right-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDGP$ to the \PNODE{} node. +\section{$\varepsilon$-rules} - % we don't have a macro of this kind - %\item{\verb+[^c[^p[@left-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ +\paragraph{Nromal Left Drop} - \item{\verb+[^c[p[!@left-open="1"][!@right-open="1"](c[!*]|i|n|o|s)*$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - replace the script with the \CNODE{} node and append the $\NLDGP$ to the \PNODE{} node. +\begin{description} -\end{description} + %************************************************************************************** + %****************************** epsilon-rules with \NLDROP **************************** + %************************************************************************************** -\paragraph{Special Left Drop:} $\SLDROP$ + %***************************** \NLDROP has no preceding nodes ************************* -%\begin{description} + \item{\verb+g[^#$]/+$\NLDROP$}\\ + replace the \G{} node with the $\NLDROP$. - %******************************************************************************************************* - %************** rules handling the case in which the cursor has a preceding node *********************** - %******************************************************************************************************* + \item{\verb+c/p[^#$]/+$\NLDROP$}\\ + remove the $\NLDROP$ and insert it before the \PNODE{} node. - %************************************************************************************************* - %*********** rules handling the case in which the cursor has no preceding nodes ****************** - %************************************************************************************************* + \item{\verb+cell[^#$]/+$\NLDROP$}\\ + replace the cell with the $\NLDROP_n$. -%\end{description} + \item{\verb+table[^#$]/+$\NLDROP$}\\ + replace the \TABLE{} node with the $\NLDROP$. -\section{Right Drop Rules} + \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 -\section{$\varepsilon$-rules} + \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\ + replace the \CNODE{} node with the $\NLDROP$. -\paragraph{Nromal Left Drop} + \item{\verb+c[^#][!p(*)]/+$\NLDROP$}\\ + replace the \CNODE{} node with the $\NLDROP$. -\begin{description} + %************************* \NLDROP has at least one preceding node ********************* + + % general rules + + % this rule should also handle the case where the \NLDROP is the third (and last) child of a script. + \item{\verb+*[*#]/+$\NLDROP$}\\ + remove the $\NLDROP$ and append it as the last child of its ex preceding brother. + + % this rule overrides the one above + \item{\verb+*[#]/+$\NLDROP$}\\ + remove the $\NLDROP$ and replace the token with the $\NLDROP_n$. + + % special rules + + \item{\verb+[^*#$]+/$\NLDROP$}\\ + replace the script node with its first child and insert the $\NLDROP$ after it. + + % this rule overrides the one above. + \item{\verb+[^g[!@id][!*]#$]/+$\NLDROP$}\\ + replace the script with the cursor. + + % this rule overrides the one above + \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\NLDROP$}\\ + remove the last \ONODE{} node and replace the $\NLDROP$ with the %$\NLDROP_n$. + + \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\NLDROP$}\\ + replace the script with its first child and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$. + + \item{\verb+c[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\ + move the $\NLDROP$ before the delimiter. + + % this rule is true for both right-open and parameterized macros. + \item{\verb+c[p#]/+$\NLDROP$}\\ + move the $\NLDROP$ into the \PNODE{} node. + + %**************************************************************************************** + %***************************** epsilon-rules with \NLDROP_n ***************************** + %**************************************************************************************** + + \item{\verb+*[*#]/+$\NLDROP_n$}\\ + replace the $\NLDROP_n$ with the cursor. - %********************* epsilon rules concerning the rgreplace_father ******************** + \item{\verb+row[cell#]/+$\NLDROP_n$}\\ + remove the $\NLDROP_n$ and append the cursor as the last child of the \CELL{} node. - \item{\verb+(g[@id][^#$]/++\verb+)+$\RGROUP$}\\ - replace the whole fragment with the cursor. + \item{\verb+row[^#$]/+$\NLDROP_n$}\\ + replace the \ROW{} node with the $\NLDROP_n$ - \item{\verb+*[!@id]/+$\RGROUP$}\\ - replace the $\RGROUP$ with the cursor. + \item{\verb+table[row#]/+$\NLDROP_n$}\\ + remove the $\NLDROP_n$ and append it as last child of the \ROW{} node. - \item{\verb+g[@id][*#]/+$\RGROUP$}\\ - replace the $\RGROUP$ with the cursor + \item{\verb+table[^#$]/+$\NLDROP_n$}\\ + replace the \texttt{table} with the cursor.$\NLDROP_n$. - \item{\verb+g[@id][#*]/+$\RGROUP$}\\ - replace the $\RGROUP$ with the cursor. - % maybe it's not the correct action + \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\ + replace the \G{} node with the $\NLDROP_n$. \end{description}