More on the presentation.

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 76cd8aa1886b02210351060e37622cc23b3a406e..44e301a79319d6f65b19db2854f709e9da20b393 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -355,6 +355,60 @@ obtained using the interpretation is refinable.
 
 \subsection{Terms at the presentation level}
 
+Content level terms are a sort of abstract syntax trees for mathematical
+expressions and proofs. The concrete syntax given to these abstract trees
+is called \emph{presentation level}.
+
+The main important difference between the content level language and the
+presentation level language is that only the former is extendible. Indeed,
+the presentation level language is a finite language that comprises all
+the usual mathematical symbols. Mathematicians invent new notions every
+single day, but they stick to a set of symbols that is more or less fixed.
+
+The fact that the presentation language is finite allows the definition of
+standard languages. In particular, for formulae we have adopt MathML
+Presentation that is an XML dialect standardized by the W3C. To visually
+represent proofs it is enough to embed formulae in plain text enriched with
+formatting boxes. Since the language of formatting boxes is very simple,
+many equivalent specifications exist and we have adopted our own, called
+BoxML.
+
+The \texttt{content\_pres} library contains the implementation of the
+translation from content level terms to presentation level terms. The
+rendering of presentation level terms is left to the application that uses
+the library. However, in the \texttt{hgdome} library we provide a few
+utility functions to build a GDOM MathML+BoxML tree from our presentation
+level terms. GDOM MathML+BoxML trees can be rendered by the GtkMathView
+widget developed by Luca Padovani \cite{gtkmathview}. The widget is
+particularly interesting since it allows to implement \emph{semantic
+selection}.
+
+Semantic selection is a technique that consists in enriching the presentation
+level terms with pointers to the content level terms and to the partially
+refined terms they correspond to. Highlight of formulae in the widget is
+constrained to selection of meaningful expressions, i.e. expressions that
+correspond to a lower level term. Once the rendering of a lower level term is
+selected it is possible for the application to retrieve the pointer to the
+lower level term. An example of applications of semantic selection is
+\emph{semantic cut\&paste}: the user can select an expression and paste it
+elsewhere preserving its semantics (i.e. the partially enriched term),
+possibly performing some semantic transformation over it (e.g. renaming
+variables that would be captured or lambda-lifting free variables).
+
+The reverse translation from presentation level terms to content level terms
+is implemented by a parser that is also found in \texttt{content\_pres}.
+Differently from the translation from content level terms to partially
+refined terms, this translation is not ambiguous. The reason is that the
+parsing library we have adopted (CamlP4) is not able to parse ambiguous
+grammars. Thus we require the mapping from presentation level terms
+(concrete syntax) to content level terms (abstract syntax) to be unique.
+This means that the user must fix once and for all the associativity and
+precedence level of every operator is he using. In prctice this limitation
+does not seem too strong. The reason is that the target of the
+translation is an ambiguous language and the user is free to associate
+to every content level term several different interpretations (as a
+partially specified term).
+
 \hrule
 
 At the bottom of the DAG we have a few libraries (\texttt{extlib},