]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/doc/spec.tex
Corrected a wrong epsilon-rule in the Special Left Drop paragraph. There was
[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex
index 1a99fdbd0cafdeb78f87fa403160bddb1277bb57..504825ae6bf8306126e5beda26f780d2c2928c6f 100644 (file)
@@ -6,10 +6,12 @@
 \usepackage{amssymb}
 \usepackage{stmaryrd}
 
-\title{A MathML Editor Based on \TeX{} Syntax\\Formal Specification}
+\title{\EdiTeX: a MathML Editor Based on \TeX{} Syntax\\\small Description and Formal Specification}
 \author{Paolo Marinelli\\Luca Padovani\\\small\{{\tt pmarinel},{\tt lpadovan}\}{\tt @cs.unibo.it}\\\small Department of Computer Science\\\small University of Bologna}
 \date{}
 
+\newcommand{\EdiTeX}{Edi\TeX}
+
 \newcommand{\tmap}[1]{\llbracket#1\rrbracket}
 \newcommand{\tadvance}{\vartriangle}
 \newcommand{\tnext}{\rhd}
 \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.
+\newcommand{\RDROP}{\vartriangleright}
 
 \begin{document}
 
 \maketitle
 
+\section{Introduction}
+
+MathML~\cite{MathML1,MathML2,MathML2E} is an XML application for the
+representation of mathematical expressions. As most XML applications,
+MathML is unsuitable to be hand-written, except for the simplest
+cases, because of its verbosity. In fact, the MathML specification
+explicitly states that
+\begin{quote}
+``While MathML is human-readable, it is anticipated that, in all but
+the simplest cases, authors will use equation editors, conversion
+programs, and other specialized software tools to generate MathML''
+\end{quote}
+
+The statement about human readability of MathML is already too strong,
+as the large number of mathematical symbols, operators, and
+diacritical marks that are used in mathematical notation cause MathML
+documents to make extensive use of Unicode characters that typically
+are not in the ``visible'' range of common text editors. Such
+characters may appear as entity references, whose name indicates
+somehow the kind of symbol used, or character references or they are
+directly encoded in the document encoding scheme (for instance,
+UTF-8).
+
+It is thus obvious that authoring MathML documents assumes the
+assistance of dedicated tools. As of today, such tools can be
+classified into two main categories:
+\begin{enumerate}
+  \item WYSIWYG (What You See Is What You Get) editors that allow the
+    author to see the formatted document on the screen as it is
+    composed;
+  \item conversion tools that generate MathML markup from different
+    sources, typically other markup languages for scientific
+    documents, such as \TeX.
+\end{enumerate}
+
+While the former tools are certainly more appealing, especially to the
+unexperienced user, as they give a direct visual feedback, the
+existance of tools in the second category takes into account the large
+availability of existing documents in \TeX{} format, and also the fact
+that experienced or ``lazy'' users may continue to prefer the use of a
+markup language other than MathML for editing, and generate MathML
+only as a final step of the authoring process. The ``laziness'' is not
+really intended as a way of being reluctant towards a new technology,
+but rather as a justified convincement that WYSIWYG editors are ``nice
+to look at'' but after all they may slow down the authoring process.
+WYSIWYG editors often involve the use of menus, palettes of symbols,
+and, in general, an extensive use of the pointing device (the mouse)
+for completing most operations. The use of shortcuts is of little
+help, as it implies very soon a challenging exercise for the fingers
+and the mind. Moreover, authors \emph{cannot improve} their authoring
+speed with time.  On the other side, the gap between the syntax of any
+markup language for mathematics and mathematical notation may be
+relevant, especially for large, non-trivial formulas and authoring is
+a re-iterated process in which the author repeadtedly types the markup
+in the editor, compiles, and looks at the result inside a pre-viewer.
+
+\EdiTeX{} tries to synthesize the ``best of both worlds'' in a single
+tool. The basic idea is that of creating a WYSIWYG editor in which
+editing is achieved by typing \TeX{} markup as the author would do in
+a text editor. The \TeX{} markup is tokenized and parsed on-the-fly
+and a corresponding MathML representation is created and
+displayed. This way, the author can see the rendered document as it
+changes. The advantages of this approach can be summarized as follows:
+\begin{itemize}
+  \item the document is rendered concurrently with the editing, the
+    user has an immediate feedback hence it is easier to spot errors;
+  \item the author types in a concrete (and likely familiar) syntax
+    improving the editing speed;
+  \item the usual WYSIWYG mechanisms are still available. In
+    particular, it is possible to select \emph{visually} a fragment of
+    the document that needs re-editing, or that was left behind for
+    subsequent editing.
+\end{itemize}
+
+\paragraph{The Name of the Game:} there is no reference to MathML in
+the name ``\EdiTeX.'' In fact, the architecture of the editor is not
+tied to MathML markup. Although we focus on MathML editing, by
+changing a completely modularized component of the editor it is
+virtually possible to generate any other markup language.
+
+\paragraph{Acknowledgments.} Stephen M. Watt and Igor Rodionov for
+their work on the \TeX{} to MathML conversion tool; Stan Devitt for an
+illuminating discussion about the architecture of \TeX{} to XML
+conversion tools; Claudio Sacerdoti Coen for the valuable feedback and
+uncountable bug reports.
+
+\section{Architecture}
+
+\section{Customization}
+
+\subsection{Short and Long Identifiers}
+
+\subsection{The Dictionary}
+
+\subsection{Stylesheets and Trasformations}
+
+\subsection{Rendering}
+
+\section{XML Representation of \TeX{} Markup}
+
 \section{Tokens}
 
 The following tokens are defined:
@@ -410,113 +509,278 @@ 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:
-  % <g id="id1"><g id="id2">...<g id="idn"><cursor/></g>...</g></g> is equivalent to:
-  % <cursor/>
+  \item{\verb+cursor+}\\
+  replace the cursor with the $\NLDROP$.
+
+\end{description}
+
+\paragraph{Special Left Drop:} $\SLDROP$
+
+\begin{description}
+
+  \item{\verb+cursor+}\\
+  replace the cursor with the $\SLDROP$.
+
+\end{description}
+
+\section{Right Drop Rules}
+
+\begin{description}
+
+  \item{\verb+cursor+}\\
+  replace the cursor with the $\RDROP$.
+
+\end{description}
+
+\section{$\varepsilon$-rules}
+
+\paragraph{Nromal Left Drop}
+
+\begin{description}
+
+  \item{\verb+math/g[^#]/+$\NLDROP$}\\
+  repalce the $\NLDROP$ with the cursor.
+
+  %**************************************************************************************
+  %****************************** epsilon-rules with \NLDROP ****************************
+  %**************************************************************************************
+
+  %**************  \NLDROP has neither preceding nor following nodes ********************
+
+  \item{\verb+math[^#$]/+$\NLDROP$}\\
+  replace the $\NLDROP$ with the cursor.
+
+  \item{\verb+g[^#$]/+$\NLDROP$}\\
+  replace the \G{} node with the $\NLDROP$.
+
+  % this rule is overridden by the two ones below
+  \item{\verb+c/p[^#$]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and insert it before the \PNODE{} node.
 
-  %************************************************************************************************************
-  %************************** there is at least one node preceding the cursor *********************************
-  %************************************************************************************************************
+  \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
 
-  %************************** cursor's parent is a group or a parameter (p node).
+  \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
+  replace the \CNODE{} node with the $\NLDROP$.
 
-  \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.
-  
-  \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+c[^#][!p(*)]/+$\NLDROP$}\\
+  replace the \CNODE{} node with the $\NLDROP$.
 
-  \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+cell[^#$]/+$\NLDROP$}\\
+  replace the cell with the $\NLDROP_n$.
 
-  \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+table[^#$]/+$\NLDROP$}\\
+  replace the \TABLE{} node with the $\NLDROP$.
 
-  \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.
+  %************************* \NLDROP has at least one preceding node *********************
 
-  % we don't have this kind of macro
-  %\item{\verb+<g|p>[c[^p[@left-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  % general rules
 
-  \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.
+  % this rule should also handles 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.
 
-  \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.
+  % this rule overrides the one above
+  \item{\verb+*[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and replace the token with the $\NLDROP_n$.
 
-  \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.
+  % special rules
 
-  %************************************ cursor's parent is a script
+  \item{\verb+<sp|sb>[^*#$]+/$\NLDROP$}\\
+  replace the script node with its first child and insert the $\NLDROP$ after it.
 
-  \item{\verb+<g|p>/<sp|sb>[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove replace the script with the cursor.
+  % this rule overrides the one above.
+  \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\NLDROP$}\\
+  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$.
+  % 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 cursor.%$\NLDROP_n$.
 
-  \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[!@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+<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.
+  \item{\verb+c[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
+  move the $\NLDROP$ before the delimiter.
 
-  % we don't have a macro of this kind
-  %\item{\verb+<sp|sb>[^c[^p[@left-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  % this rule is true for both right-open and parameterized macros.
+  \item{\verb+c[p#]/+$\NLDROP$}\\
+  move the $\NLDROP$ into the \PNODE{} node.
 
-  \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.
+  %**************** \NLDROP has no preceding nodes, but has following nodes **************
+
+  % general rule
+  \item{\verb+*[^#*]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and insert it before its parent.
+
+  % special rules
+
+  % this rule is applicable to all macros.
+  \item{\verb+c[^#][p[*]]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and insert it before the \CNODE{} node.
 
 \end{description}
 
-\paragraph{Special Left Drop:} $\SLDROP$
+\paragraph{Special Left Drop}
 
-%\begin{description}
+\begin{description}
 
-  %*******************************************************************************************************
-  %************** rules handling the case in which the cursor has a preceding node ***********************
-  %*******************************************************************************************************
+  %********************************************************************************************************
+  %************************************ epsilon-rules with \SLDROP ****************************************
+  %********************************************************************************************************
 
-  %*************************************************************************************************
-  %*********** rules handling the case in which the cursor has no preceding nodes ******************
-  %*************************************************************************************************
+  \item{\verb+math/+$\SLDROP$}\\
+  replace the $\SLDROP$ with the cursor.
 
-%\end{description}
+  \item{\verb+math/g[^#]/+$\NLDROP$}\\
+  replace the $\NLDROP$ with the cursor.
 
-\section{Right Drop Rules}
+  %************************ \SLDROP has neither preceding nor following nodes *****************************
 
-\section{$\varepsilon$-rules}
+  \item{\verb+g[^#$]/+$\SLDROP$}\\
+  replace the \G{} node with the cursor.
 
-\paragraph{Nromal Left Drop}
+  \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
+  replace the \CNODE{} node with the content of the first \PNODE{} node and insert the cursor after this content
+
+  \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
+  replace the \CNODE{} node with the cursor.
+
+  \item{\verb+c/p[^#$]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and insert it before the \PNODE{} node.
+
+  \item{\verb+c[^#][!p(*)]/+$\SLDROP$}\\
+  replace the \CNODE{} node with the cursor.
+
+  \item{\verb+cell[^#$]/+$\SLDROP$}\\
+  replace the cell with the $\NLDROP_n$.
+
+  \item{\verb+table[^#$]/+$\SLDROP$}\\
+  replace the \TABLE{} node with the cursor.
+
+  %*********************** \SLDROP has at least one preceding node ***********************************
+
+  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\SLDROP$}\\
+  remove the last \ONODE{} node and replace the $\SLDROP$ with the cursor.
+
+  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\SLDROP$}\\
+  replace the script with its first child and replace the $\SLDROP$ with the cursor.%$\NLDROP_n$.
+
+  \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\SLDROP$}\\
+  replace the script with the cursor.
+
+  % this rule is overridden by the three rules above.
+  \item{\verb+<sp|sb>[^*#$]+/$\SLDROP$}\\
+  replace the script node with its first child and insert the cursor after it.
+
+  \item{\verb+c[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and insert the cursor before the delimiter.
+
+  \item{\verb+c[p#(i|n|o|s|c[!*])]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and insert the cursor into the \PNODE{} node.
+
+  \item{\verb+c[p[@right-open='1']#]+}\\
+  remove the $\SLDROP$ and append the curor as last child of the \PNODE{} node.
+
+  % this rule is overridden by the two ones above.
+  \item{\verb+c[p#]/+$\SLDROP$}\\
+  move the $\SLDROP$ into the \PNODE{} node.
+
+  \item{\verb+*[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and replace the token with the cursor.
+
+  \item{\verb+*[table#]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and append the $\NLDROP_n$ as the last child of the \TABLE{} node.
+
+  \item{\verb+*[c#]/+$\SLDROP$}\\
+  move the $\SLDROP$ into the \CNODE{} node.
+
+  \item{\verb+*[g#]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and append the cursor as the last child of the \G{} node.
+
+  %********** \SLDROP has no preceding node, but has following ones **************
+
+  \item{\verb+c[^#p][p(*)]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and insert the cursor before the \CNODE{} node.
+
+  % general rule
+  \item{\verb+*[^#*]/+$\SLDROP$}\\
+  remove the $\SLDROP$ and insert the cursor before its parent.
+
+\end{description}
+
+\paragraph{Normalize Left Drop}
 
 \begin{description}
 
-  %********************* epsilon rules concerning the rgreplace_father ********************
+  %****************************************************************************************
+  %***************************** epsilon-rules with \NLDROP_n *****************************
+  %****************************************************************************************
 
-  \item{\verb+(g[@id][^#$]/++\verb+)+$\RGROUP$}\\
-  replace the whole fragment with the cursor.
+  \item{\verb+*[*#]/+$\NLDROP_n$}\\
+  replace the $\NLDROP_n$ with the cursor.
 
-  \item{\verb+*[!@id]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor.
+  \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][*#]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor
+  \item{\verb+row[^#$]/+$\NLDROP_n$}\\
+  replace the \ROW{} node with the $\NLDROP_n$
 
-  \item{\verb+g[@id][#*]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor.
-  % maybe it's not the correct action
+  \item{\verb+table[row#]/+$\NLDROP_n$}\\
+  remove the $\NLDROP_n$ and append it as last child of the \ROW{} node.
+
+  \item{\verb+table[^#$]/+$\NLDROP_n$}\\
+  replace the \TABLE{} with the cursor.%$\NLDROP_n$.
+
+  \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\
+  replace the \G{} node with the $\NLDROP_n$.
+
+  \item{$\NLDROP_n$}\\
+  replace the $\NLDROP_n$ with the cursor.
 
 \end{description}
 
-\paragraph{Special Left Drop}
+\paragraph{Right Drop}
+
+\begin{description}
+
+  %************************* \RDROP has at least a following node ****************************************
+
+  \item{\verb+c[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
+  remove the $\RDROP$ and append it after the delimiter
+
+  \item{\verb+*[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
+  remove the token and replace the $\RDROP$ with the cursor $\RDROP_n$.
+
+  % this rule is overridden by those ones above.
+  \item{\verb+*[#*]/+$\RDROP$}\\
+  remove the $\RDROP$ and append it as the first child of the following node.
+
+  %************************** \RDROP has neither following nor preceding nodes ******************************
 
-%\begin{description}
+  \item{\verb+c[#$][!p[*]]/+$\RDROP$}\\
+  replace the \CNODE{} with the $\RDROP$.
 
-%\end{description}
+  \item{\verb+p[^#$]/+$\RDROP$}\\
+  move the $\RDROP$ after the \PNODE{} node.
+
+  \item{\verb+g[^#$]/+$\RDROP$}\\
+  replace the \G{} node with the $\RDROP$.
+
+\end{description}
+
+\paragraph{Normalize Right Drop}
+
+\begin{description}
+
+  % at the moment it's the only rule, defined for this symbol.
+  \item{\verb+g[@id][^#$]/+$\RDROP_n$}\\
+  replace the \G{} node with the $\RDROP_n$.
+
+  \item{$\RDROP_n$}\\
+  replace the $\RDROP$ with the cursor.
+
+\end{description}
 
 \paragraph{Advance}