+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}. At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof General
+based on Eclipse, but is not yet the case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation.
+
+The foreground window, also implemented around \GTKMATHVIEW, is called
+``cicBrowser''. It is used to browse the library, including the proof being
+developed, and enable content based search over it. Proofs are rendered in
+natural language, automatically generated from the low-level lambda-terms,
+using techniques inspired by \cite{natural,YANNTHESIS} and already described
+in~\cite{remathematization}.
+
+Note that the syntax used in the script view is \TeX-like, however unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]