From: Paolo Marinelli Date: Fri, 28 Mar 2003 12:32:23 +0000 (+0000) Subject: Added some rules in the "Left Drop" section. X-Git-Tag: before_refactoring~80 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a945fbcad6168b7872d16a65860a07d936c2f10;p=helm.git Added some rules in the "Left Drop" section. Dropped some obsolete rules. --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 80ce0dd6b..1a99fdbd0 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -28,6 +28,9 @@ \newcommand{\SLDROP}{\blacktriangleleft} \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. \begin{document} @@ -407,8 +410,6 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \begin{description} - %********* rules that try to express situations completely specified (there is an effective deletion) ****** - % 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). @@ -417,223 +418,74 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node % ...... is equivalent to: % - \item{\verb+[(i|n|o|s|c[ ])#]/(g[@id][^#$]/++\verb+)?cursor+}\\ + %************************************************************************************************************ + %************************** there is at least one node preceding the cursor ********************************* + %************************************************************************************************************ + + %************************** cursor's parent is a group or a parameter (p node). + + \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$. \item{\verb+[g#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append $\NLDG$ to the \G{} node preceding the cursor - - %% there is an optional sequence of groups with id, all of which having one and only one child. The last - %% child of this sequence (or the root, if the sequence is empty) is a group with id, has as first element a - %% token and has as second and last element an eventually empty sequence of groups with id, all of which having - %%one and only one child. The last element of this sequence has the cursor as its child. - %\item{\verb+(g[@id][^#$]/++\verb+)?g[@id][^(i|n|o|s|c[ ])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ - %replace the whole fragment with the cursor. - - % the cursor is a macro's child. There is an eventually empty sequence of delimiters, which precedes the - % cursor. Before this sequence, there is a p node. This p node has as its last child a token - \item{\verb+c[p[(i|n|o|s|c[ ])$]((i|n|o|s|c[ ])*)#]/cursor+}\\ - remove the cursor and replace the token with the cursor. - - % there is a token, which precedes the cursor. The cursor is child of either a group or a parameter. - % the case where the cursor is child of a group with id, there are no nodes after the cusror and there - % are no nodes preceding the token, is handled by the first rule. - % This rule is duplicated below, but that one could have a wrong syntax. This one has been tested. - \item{\verb+[(i|n|o|c[ ])#]/cursor+}\\ - remove the cursor and replace the token with the cursor. - - % cursor's parent is a script (the cursor is not the base). The script's base is an empty group with id. - % The script is preceded by a token.The script's parent is group or a parameter. - % The case where the script's parent is a group with id and the token is the first child, while - % the script is the last one, is handled some rules later. - \item{\verb+[(i|n|o|s|c[ ])#]/[^(g[@id][ ])#$]/cursor+}\\ - remove the script and replace the token with the cursor. - - % As above, but: we don't care who precedes the script (we do not have to remove it); the script's base - % is still an empty group, but it has no id. - % Ad above, we have to precise that the situation where the script is the only child of a group with id - % is handled some rules later. - \item{\verb+/[^(g[!@id][ ])#$]/curosr+}\\ - replace the script with the cursor. - - % The cursor is the last child of a script. The script's base is token. - \item{\verb+/[^(i|n|o|s|c[ ])#$]/cursor+}\\ - repalce the script with the 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. - %************************* the cursor's parent is a group or a parameter ******************************* - - %we consider an empty macro as a token. An empty macro is either undefined or simply empty. - - %rule handling the case where the cursor has a preceding token and this is the first node of a group with id - \item{\verb+g[@id][^(i||n||o||s||c[^$])#]/cursor+}\\ - remove the cursor and replace the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node with the $\NLDROP$. - \item{\verb+[(i||n||o||s||c[^$])#]/cursor+}\\ - remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node. - %it corresponds to the drop_prev_group(false). - \item{\verb+[g#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \G{} node. - %corresponds to the drop_prev_script(false). - \item{\verb+[()#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \SP{} or \SB{} node. - %rules handling the right open macros preceding the cursor. - \item{\verb+[(c[^p[@right-open='1']$])#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \PNODE{} node. - %we don't have a macro of this kind, but we don't know the future... - \item{\verb+[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\ - remove the cursor and replace the \CNODE node with the $\NLDROP$. - \item{\verb+[(c[^p[!(@right-open='1')][@left-open='1']$])#]/cursor+}\\ - replace the \CNODE{} node with the content of the \PNODE node and replace the cursor with the $\NLDROP$. - %rules handling macro with parameter(s) and preceding the cursor. - \item{\verb+[c#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \CNODE{} node. - %rule handling table with rows preceding the cursor. - \item{\verb+[(table[row[cell[^g$]$]$])#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \G{} node, which is child of the \CELL{} node. - %rule handling tables without rows preceding the cursor. - \item{\verb+[table#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the \TABLE{} node - - %********************************* the cursor's parent is a script ****************************** - - %rule handling the case where the script's base is an empty group with id. - \item{\verb+[^(g[@id][^$])#$]/cursor+}\\ - replace the \SP{} or \SB{} node with the $\NLDROP$. - %rule handling the case where the script's base is an empty group without id - \item{\verb+[^(g[^$])#$]/cursor+}\\ - replace the \SP{} or \SB{} node with the cursor. - %rule handling the case where the script's base is something else - \item{\verb+[^*#$]/cursor+}\\ - replace the \SP{} or \SB{} node with it's first child and insert the $\NLDROP$ after it. - - %********************************* the cursor's parent is a macro ******************************** - - %rule handling the case where the preceding node is a parameter - \item{\verb+c[p#]/cursor+}\\ - remove the cursor and append the $\NLDROP$ to the PNODE{} node. - %rule handling the case where the preceding node is a delimiter - \item{\verb+c[()#]/cursor+}\\ - remove the cursor and insert the $\NLDROP$ before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} 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. - %************************************************************************************************* - %*********** rules handling the case in which the cursor has no preceding nodes ****************** - %************************************************************************************************* + % we don't have this kind of macro + %\item{\verb+[c[^p[@left-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\ - %rule handling the case where the cursor has something else after it - \item{\verb+[#*]/cursor+}\\ - nothing to drop. - - %rules handling the case where the cursor's parent is a p node and the cursor has no nodes after it. - - %rule handling the case where the p node is a left and right open macro's child and the first p node has no elements. - \item{\verb+c[^(p[@left-open='1'][^$])#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the $\NLDROP$. - %rule handling the case where the p node is a left and right open macro's child and the first p node has elements. - \item{\verb+c[^(p[@left-open='1']#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the content of the PNODE{} with attribute texttt{left-open='1'} and insert $\NLDROP$ after this. - %rule handling the case where the p node is right open macro's child. - \item{\verb+c[^#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the $\NLDROP$. - %rule handling the case where the p node is a macro's child and this macro has parameter. - \item{\verb+c/p[^#$]/cursor+}\\ - remove the cursor and insert the $\NLDROP$ before the \PNODE{} node. - - %rule handling the case where the cursor has no nodes after it and its parent is a group with id - \item{\verb+g[@id][^#$]/cursor+}\\ - replace the \G{} node with the $\NLDROP$. + \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+*[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+*[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. + + %************************************ cursor's parent is a script + + \item{\verb+/[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ + remove replace the script with the cursor. + + \item{\verb+g[@id]/[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ + replace the script with the $\RGROUP$. + + \item{\verb+[g#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ + repalce the script with it's first child (the \G{} node) and append the $\NLDGP$ to it. + + \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. + + % we don't have a macro of this kind + %\item{\verb+[^c[^p[@left-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\ + + \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. \end{description} \paragraph{Special Left Drop:} $\SLDROP$ -\begin{description} +%\begin{description} %******************************************************************************************************* %************** rules handling the case in which the cursor has a preceding node *********************** %******************************************************************************************************* - %************************* the cursor's parent is a group or a parameter ******************************* - - %this rule is more specific than the one below which handle the case of the cursor preceded by a c node - \item{\verb+[(i||n||o||s||c[^$])#]/cursor+}\\ - remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node. - %it corresponds to the drop_prev_group(true). - \item{\verb+[g#]/cursor+}\\ - remove the cursor and append the it to the \G{} node. - %corresponds to the drop_prev_script(true). - \item{\verb+[()#]/cursor+}\\ - remove the cursor and append the $\SLDROP$ to the \SP{} or \SB{} node. - %rules handling the right open macros preceding the cursor. - \item{\verb+[(c[^p[@right-open='1']$])#]/cursor+}\\ - remove the cursor and append the $\SLDROP$ to the \PNODE{} node. - %we don't have a macro of this kind, but we don't know the future... - \item{\verb+[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\ - remove the cursor and replace the \CNODE node with the cursor. - \item{\verb+[(c[^p[!(@right-open='1')][@left-open='1']$])#]/cursor+}\\ - replace the \CNODE{} node with the content of the \PNODE node. - %rule handling macro with parameter(s) and preceding the cursor. - \item{\verb+[c#]/cursor+}\\ - remove the cursor and append the $\SLDROP$ to the \CNODE{} node. - %rule handling table with rows preceding the cursor. - \item{\verb+[(table[row[cell[^g$]$]$])#]/cursor+}\\ - remove the cursor and append the it to the \G{} node, which is child of the \CELL{} node. - %rule handling tables without rows preceding the cursor. - \item{\verb+[table#]/cursor+}\\ - remove the cursor and append the $\SLDROP$ to the \TABLE{} node - - %********************************* the cursor's parent is a script ****************************** - - %rule handling the case where the script's base is an empty group with id. - \item{\verb+[^(g[@id][^$])#$]/cursor+}\\ - replace the \SP{} or \SB{} node with the \G{} node and insert the cursor after it. - %rule handling the case where the script's base is an empty group without id - \item{\verb+[^(g[^$])#$]/cursor+}\\ - replace the \SP{} or \SB{} node with the cursor. - %rule handling the case where the scrip's base is something else - \item{\verb+[^*#$]/cursor+}\\ - replace the \SP{} or \SB{} node with it's first child and insert the cursor after it. - - %********************************* the cursor's parent is a macro ******************************** - - %rule handling the case where the preceding node is a parameter - \item{\verb+c[p#]/cursor+}\\ - remove the cursor and append the $\SLDROP$ to the PNODE{} node. - %rule handling the case where the preceding node is a delimiter - \item{\verb+c[()#]/cursor+}\\ - remove the cursor and insert the it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node. - %************************************************************************************************* %*********** rules handling the case in which the cursor has no preceding nodes ****************** %************************************************************************************************* - %rule handling the case where the cursor has something else after it - \item{\verb+[#*]/cursor+}\\ - nothing to drop. - - %rules handling the case where the cursor's parent is a p node and the cursor has no nodes after it. - - %rule handling the case where the p node is a left and right open macro's child and the first p node has no elements. - \item{\verb+c[^(p[@left-open='1'][^$])#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the cursor. - %rule handling the case where the p node is a left and right open macro's child and the first p node has elements. - \item{\verb+c[^(p[@left-open='1']#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the content of the PNODE{} with attribute texttt{left-open='1'} and insert cursor after this. - %rule handling the case where the p node is right open macro's child. - \item{\verb+c[^#$]/p[@right-open='1'][^#$]/cursor+}\\ - replace the \CNODE{} with the cursor. - %rule handling the case where the p node is a macro's child and this macro has parameter. - \item{\verb+c/p[^#$]/cursor+}\\ - remove the cursor and insert the $\SLDROP$ before the \PNODE{} node. - - %rule handling the case where the cursor has no nodes after it and its parent is a group with id - \item{\verb+g[@id][^#$]/cursor+}\\ - replace the \G{} node with the cursor. - -\end{description} +%\end{description} \section{Right Drop Rules} @@ -658,91 +510,13 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node replace the $\RGROUP$ with the cursor. % maybe it's not the correct action - - - %********************************************* \NLDROP has a preceding node ********************************************* - - %rule handling the case where the preceding node is a token or an empty macro. - \item{\verb+*[(i||n||o||s||c[^$])#]/+$\NLDROP$}\\ - remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or the \CNODE{} node. - %rule handling the case where the preceding node is a group - \item{\verb+*[g#]/+$\NLDROP$}\\ - remove the $\NLDROP$ append it to the \G{} node. - %rule handling the case where the preceding node is a script - \item{\verb+*[#]/+$\NLDROP$}\\ - remove the $\NLDROP$ append it to the \SP{} or \SB{} node. - %rule handling the case where the preceding node is an open-right macro - \item{\verb+*[(c[^p[@right-open='1']$])#]/+$\NLDROP$}\\ - remove the $\NLDROP$ and append it to the \PNODE{} node. - %rule handling the case where the preceding node is a left-open macro (and not right-open), and the p node of this macro has no children - \item{\verb+*[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/+$\NLDROP$}\\ - remove the \CNODE node. - %rule handling the case where the preceding node is a left-open macro (and not right-open), and the p node of this macro has children - \item{\verb+*[(c[^p[!(@right-open='1')][@left-open='1']$])#]/+$\NLDROP$}\\ - replace the \CNODE{} node with the content of the \PNODE{} node. - %rule handling the case where the preceding node is a macro with parameter(s) - \item{\verb+*[c#]/+$\NLDROP$}\\ - remove the $\NLDROP$ and append it to the \CNODE{} node. - - %rule handling the deletion of primes in superscript - - %there are more than one prime in the phantom group - \item{\verb+sp[!(@id)][*#$]/g[!(@id)][o#]/+$\NLDROP$}\\ - remove the \ONODE node, remove the $\NLDROP$ and insert the cursor after the \SP{} node. - %there is one and only one prime in the phantom group - \item{\verb+sp[!(@id)][*#$]/g[!(@id)][^o#]/+$\NLDROP$}\\ - replace the \SP{} node with it's first child and insert the cursor after it - - %*** rules handling the case where the \NLDROP's parent is a macro (with parameter) *** - - %the node preceding the \NLDROP is a delimiter - \item{\verb+c[()#]/+$\NLDROP$}\\ - remove the $\NLDROP$ and insert it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node. - %the node preceding the \NLDROP is parameter - \item{\verb+c[p#]/+$\NLDROP$}\\ - remove the $\NLDROP$ and append it to the \PNODE{} node. - - %********************************************* the \NLDROP has no preceding nodes **************************************************** - - %if the \NLDROP has no preceding nodes, but has following nodes... - \item{\verb+[#*]/+$\NLDROP$}\\ - replace the $\NLDROP$ with the cursor. - %rule handling the case where the $\NLDROP$ is the only child of a group with id. - \item{\verb+g[@id][^#$]/+$\NLDROP$}\\ - replace the \G{} node with the $\NLDROP$. - %\NLDROP is the first child of a macro with no inserted parameter - \item{\verb+c[!(p[*])][^#]/+$\NLDROP$}\\ - replace the \CNODE{} with the $\NLDROP$. - %\NLDROP is the first child of a macro with some inserted parameter - \item{\verb+c[p[*]][^#]/+$\NLDROP$}\\ - put the cursor in the first \PNODE{} node. - - - %**** rule handling the case where the \NLDROP has a preceding token or a preceding empty macro, which is either undefined or empty **** - - %%the \NLDROP's parent is neither a macro nor a phantom group which in turn is a sp's child and the token is a prime - %\item{\verb+*[(i||n||o||s||c[^$])#]/+$\NLDROP$}\\ - %replace the \INODE{}, \NNODE{}, \SNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node with the cursor and remove the $\NLDROP$. - %%the \NLDROP's parent is a macro with argument - %\item{\verb+c[((!(p[@left-open='1']))&(!(p[@right-open+'1'])))][(i||n||o||s||c[^$])#]/+$\NLDROP$}\\ - %remove the $\NLDROP$ and insert it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node. - %%rule handling the case where the \NLDROP's parent is a phantom group, which in turn is a sp's child - %\item{\verb+sp[!(@id)][^*#$]/g[!(@id)][o#$]/+$\NLDROP$}\\ - %remove the \ONODE{} node - - %********************************* rules handling the case where the \NLDROP has a preceding group ************************************** - \item{\verb+*[g#]/+$\NLDROP$}\\ - remove the $\NLDROP$ and append it to the \G{} node. - \end{description} \paragraph{Special Left Drop} -\begin{description} - - \item{special left}\\ +%\begin{description} -\end{description} +%\end{description} \paragraph{Advance}