]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/doc/spec.tex
Added some rules in the "Left Drop" section.
[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex
index de575c719ebb8887ce3d490da901cf854716eb50..1a99fdbd0cafdeb78f87fa403160bddb1277bb57 100644 (file)
 \newcommand{\ROW}{\texttt{row}}
 \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}
 
@@ -406,179 +410,82 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
 \begin{description}
 
-  %*******************************************************************************************************
-  %************** rules handling the case in which the cursor has a preceding node ***********************
-  %*******************************************************************************************************
+  % 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:
+  % <g id="id1"><g id="id2">...<g id="idn"><cursor/></g>...</g></g> is equivalent to:
+  % <cursor/>
 
-  %************************* 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+<g|p>[(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|p>[g#]/cursor+}\\
-  remove the cursor and append the $\NLDROP$ to the \G{} node.
-  %corresponds to the drop_prev_script(false).
-  \item{\verb+<g|p>[(<sp|sb>)#]/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+<g|p>[(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+<g|p>[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\
-  remove the cursor and replace the \CNODE node with the $\NLDROP$.
-  \item{\verb+<g|p>[(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+<g|p>[c#]/cursor+}\\
-  remove the cursor and append the $\NLDROP$ to the \CNODE{} node.
-  %rule handling table with rows preceding the cursor.
-  \item{\verb+<g|p>[(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+<g|p>[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+<sp|sb>[^(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+<sp|sb>[^(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+<sp|sb>[^*#$]/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[(<i|n|o|s|c>)#]/cursor+}\\
-  remove the cursor and insert the $\NLDROP$ before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
+  %************************************************************************************************************
+  %************************** there is at least one node preceding the cursor *********************************
+  %************************************************************************************************************
 
-  %*************************************************************************************************
-  %*********** rules handling the case in which the cursor has no preceding nodes ******************
-  %*************************************************************************************************
+  %************************** cursor's parent is a group or a parameter (p node).
 
-  %rule handling the case where the cursor has something else after it
-  \item{\verb+<g|p>[#*]/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.
+  \item{\verb+<g|p>[(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.
   
-  %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+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|p>[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.
+
+  \item{\verb+<g|p>[<sp|sb>#]/(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.
+
+  \item{\verb+<g|p>[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.
+
+  % we don't have this kind of macro
+  %\item{\verb+<g|p>[c[^p[@left-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
+
+  \item{\verb+<g|p>[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+<g|p>/<sp|sb>[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  remove replace the script with the cursor.
+
+  \item{\verb+g[@id]/<sp|sb>[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  replace the script with the $\RGROUP$.
+
+  \item{\verb+<sp|sb>[g#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  repalce the script with it's first child (the \G{} node) and append the $\NLDGP$ to it.
+
+  \item{\verb+<sp|sb>[^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+<sp|sb>[^c[^p[@left-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+
+  \item{\verb+<sp|sb>[^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+<g|p>[(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|p>[g#]/cursor+}\\
-  remove the cursor and append the it to the \G{} node.
-  %corresponds to the drop_prev_script(true).
-  \item{\verb+<g|p>[(<sp|sb>)#]/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+<g|p>[(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+<g|p>[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\
-  remove the cursor and replace the \CNODE node with the cursor.
-  \item{\verb+<g|p>[(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+<g|p>[c#]/cursor+}\\
-  remove the cursor and append the $\SLDROP$ to the \CNODE{} node.
-  %rule handling table with rows preceding the cursor.
-  \item{\verb+<g|p>[(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+<g|p>[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+<sp|sb>[^(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+<sp|sb>[^(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+<sp|sb>[^*#$]/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[(<i|n|o|s|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+<g|p>[#*]/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}
 
@@ -588,90 +495,28 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
 \begin{description}
 
+  %********************* epsilon rules concerning the rgreplace_father ********************
 
-  %********************************************* \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+*[<sp|sb>#]/+$\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[(<i|n|o|s|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+<g|p>[#*]/+$\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.
-  
+  \item{\verb+(g[@id][^#$]/++\verb+)+$\RGROUP$}\\
+  replace the whole fragment with the cursor.
 
-  %**** rule handling the case where the \NLDROP has a preceding token or a preceding empty macro, which is either undefined or empty ****
+  \item{\verb+*[!@id]/+$\RGROUP$}\\
+  replace the $\RGROUP$ with the cursor.
 
-  %%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
+  \item{\verb+g[@id][*#]/+$\RGROUP$}\\
+  replace the $\RGROUP$ with the cursor
 
-  %********************************* 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.
+  \item{\verb+g[@id][#*]/+$\RGROUP$}\\
+  replace the $\RGROUP$ with the cursor.
+  % maybe it's not the correct action
 
 \end{description}
 
 \paragraph{Special Left Drop}
 
-\begin{description}
-
-  \item{special left}\\
+%\begin{description}
 
-\end{description}
+%\end{description}
 
 \paragraph{Advance}