+\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.
+
+\section{Library Management}
+
+\subsection{Indexing and searching}
+
+
+\subsection{Compilation and decompilation}
+\label{compilazione}
+
+The aim of this section is to describe the way matita
+preserves the consistency and the availability of the library
+trough the \WHELP{} technology, in response to the user addition or
+deletion of mathematical objects.
+
+As already sketched in \ref{fully-spec} the output of the
+compilation of a script is split among two storage media, a
+classical filesystem and a relational database. The former is used to
+store the XML encoding of the objects defined in the script, the
+disambiguation aliases and the interpretation and notational convention defined,
+while the latter is used to store all the metadata needed by
+\WHELP{}. In addition the \emph{getter} component
+should be updated with the the new mapping between the logical URI
+and the physical path of objects.
+
+While this kind of consistency has nothing to do with the nature of
+the content of the library and is thus of poor interest (but really
+tedious to implement and keep bug-free), there is a more deep
+notion of mathematical consistency we need to provide. Each object
+must reference only defined object (i.e. each proof must use only
+already proved theorems).
+
+We will focus on how matita ensures the interesting kind
+of consistency during the formalization of a mathematical theory,
+giving the user the freedom of adding, deleting, modifying objects
+without loosing the feeling of an always visible and browsable
+library.
+
+\subsubsection{Compilation}
+The typechecker component guarantees that if an object is well typed
+it depends only on well defined objects available in the library,
+that is exactly what we need to be sure that the logic consistency of
+the library is preserved. We have only find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we developed a low level tool called \emph{matitadep}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the make utility.
+The user is not asked to run \emph{matitadep} nor make by hand, but
+simply to tell matita the root directory of his development (where all
+script files can be found) and matita will handle all the compilation
+tasks.\\
+To calculate dependencies it is enough to look at the script file for
+its inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{aliases}).
+
+The output of the compilation is immediately available to the user
+trough the \WHELP{} technology, since all metadata are stored in a
+user-specific area of the database where the search engine has read
+access, and all the automated tactics that operates on the whole
+library, like auto, have full visibility of the newly defined objects.
+
+Compilation is rather simple, and the only tricky case is when we want
+to compile again the same script, maybe after the deletion of a
+theorem. Here the policy is simple: decompile it before recompiling.
+As we will see in the next section decompilation will ensure that
+there will be no theorems in the development that depends on the
+removed item.
+
+\subsubsection{Decompilation}
+Decompiling an object involves,
+recursively, the decompilation of all the objects that depend on it.
+
+The calculation of the reverse dependencies can be computed in two
+ways, using the relational database or using a simpler set of metadata
+that matita saves in the filesystem as a result of compilation. The
+former technique is the same used by the \emph{Dependency Analyzer}
+described in \cite{zack-master} and really depends on a relational
+database.\\
+The latter is a fall-back in case the database is not available. Due to
+the complex deployment of a complex peace of software like a database,
+it is a common usage for the \HELM{} team to use a single and remote
+database, that may result unavailable if the user workstation lacks
+connectivity. This facility has to be intended only as a fall-back,
+since the whole \WHELP{} technology depends on the database.
+
+Decompilation guarantees that if an object is removed there are no
+dandling references to it, and that the part of the library still
+compiled is logically consistent. Since decompilation involves the
+deletion of all the outputs of the compilation, metadata included, the
+library browsable trough the \WHELP{} technology is always up to date.
+
+\subsubsection{Interactive and batch (de)compilation}
+Matita includes an interactive graphical interface and a batch
+compiler. Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a not yet compiled
+part of the user development is required.
+
+While they share the same engine for compilation and decompilation,
+they provide different granularity. The batch compiler is only able to
+compile a whole script file and reciprocally it can decompile only a whole
+script, and consequently all the other scripts that rely on an object
+defined in it. The interactive interface is able to execute single steps
+of compilation, that may include the definition of an object, and
+symmetrically to undo single steps, thus removing single objects.
+
+%
+%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
+%\subsubsection{Composition}
+%scripts.ma, .moo, XML, metadata
+%\subsubsection{Compilation}
+%analogie con compilazione classica dso.\\
+%granularita' differenti per uso interattivo e non
+%\paragraph{Batch}
+%- granularita' .ma/buri \\
+%-- motivazioni\\
+%- come si calcolano le dipendenze\\
+%- quando la si usa\\
+%- metodi (cc e clean)\\
+%- garanzie
+%\paragraph{Interactive}
+%- granularita' fine\\
+%-- motivazioni
+%\label{sec:libmanagement}
+%consistenza: integrita' referenziale
+%Goals: mantenere consistente la rappresentazione della libreria su memoria persistente consentendo di compilare e decompilare le compilation unit (.ma).\\
+%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
+%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
+%--- granularita' oggetto per matita interactive\\
+%--- granularita' baseuri (compilation unit) per la libreria\\
+%In entrmbi i casi ora:\\
+%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
+%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
+%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
+%Vincoli di remove: \\
+%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
+%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
+%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
+%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
+
+\subsection{Automation}