From: Paolo Marinelli Date: Mon, 31 Mar 2003 16:00:33 +0000 (+0000) Subject: Added some examples of Right Drop. X-Git-Tag: before_refactoring~73 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=055e81ccd1910f00a291c5f035bf9907ea8f6959;p=helm.git Added some examples of Right Drop. --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 4495c805e..9dfc6ec24 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -29,6 +29,7 @@ \newcommand{\ROW}{\texttt{row}} \newcommand{\SLDROP}{\blacktriangleleft} \newcommand{\NLDROP}{\vartriangleleft} +\newcommand{\RDROP}{\vartriangleright} \begin{document} @@ -524,6 +525,13 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \section{Right Drop Rules} +\begin{description} + + \item{\verb+cursor+}\\ + replace the cursor with the $\RDROP$. + +\end{description} + \section{$\varepsilon$-rules} \paragraph{Nromal Left Drop} @@ -737,6 +745,28 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \end{description} +\paragraph{Right Drop} + +\begin{description} + + \item{\verb+c[#(i|n|o|s|c[!*])]/+$\RDROP$}\\ + remove the $\RDROP$ and append it after the delimiter + + \item{\verb+*[#$]/+$\RDROP$}\\ + remove the $\RDROP$ and insert it after its parent. + + \item{\verb+*[#(i|n|o|s|c[!*])]/+$\RDROP$}\\ + remove the token and replace the $\RDROP$ with the $\RDROP_n$. + + \item{\verb+*[#]+}\\ + ? + + % this rule is overridden bu those above. + \item{\verb+*[#*]/+$\RDROP$}\\ + remove the $\RDROP$ and append it as the first child of the following node. + +\end{description} + \paragraph{Advance} \begin{description}