-In particular, the \texttt{xml} \component{} is used
-to easily represent, parse and pretty-print XML files.
-
-\section{Using \MATITA (boh \ldots cambiare titolo)}
-
-\begin{figure}[t]
- \begin{center}
-% \includegraphics[width=0.9\textwidth]{a.eps}
- \caption{\MATITA{} screenshot}
- \label{fig:screenshot}
- \end{center}
-\end{figure}
-
-\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
-split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a MathML rendering
-widget. A distinguished part of the script (shaded in the screenshot) represent
-the commands already executed and can't be edited without undoing them. The
-remaining part can be freely edited and commands from that part can be executed
-moving down the execution point. An additional window --- the ``cicBrowser'' ---
-can be used to browse the library, including the proof being developed, and
-enable content based search on it. In the cicBrowser proofs are rendered in
-natural language, automatically generated from the low-level $\lambda$-terms
-using techniques inspired by \cite{natural,YANNTHESIS}.
-
-In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
-only seen as a convenient way to create mathematical objects. The universe of
-all these objects makes up the \HELM{} library, which is always completely
-visible to the user. The mathematical library is thus conceived as a global
-hypertext, where objects may freely reference each other. It is a duty of
-the system to guide the user through the relevant parts of the library.
-
-This methodological assumption has many important consequences
-which will be discussed in the next section.
-
-%on one side
-%it requires functionalities for the overall management of the library,
-%%%%%comprising efficient indexing techniques to retrieve and filter the
-%information;
-%on the other it introduces overloading in the use of
-%identifiers and mathematical notation, requiring sophisticated disambiguation
-%techniques for interpreting the user inputs.
-%In the next two sections we shall separately discuss the two previous
-%points.
-
-%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
-%organized in components which work on data in this format. For instance the
-%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%MathML Presentation documents, can be used apart from \MATITA{} to print ...
-%FINIRE
-
-A final section is devoted to some innovative aspects
-of the authoring system, such as a step by step tactical execution,
-content selection and copy-paste.