From: Paolo Marinelli <paolo.marinelli@unibo.it>
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;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+*[#<sp|sb>]+}\\
+  ?
+
+  % 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}