reshaped the "authoring interface" part

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 192117af50dd9c14139cddad54e7adf7c11301a4..802bcfa372589fc571768fd2c541b0209a197f54 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -60,7 +60,7 @@
 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
 
 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
 
 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black

-\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+\newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}

 \newcommand{\URI}[1]{\texttt{#1}}
 \newcommand{\OP}[1]{``\texttt{#1}''}
 
 \newcommand{\URI}[1]{\texttt{#1}}
 \newcommand{\OP}[1]{``\texttt{#1}''}
 


@@ -228,7 +228,8 @@ for human audiences).
 The user interfaces now adopted by all the proof assistants that adopt a
 procedural proof language have been inspired by the CtCoq pioneering
 system~\cite{ctcoq}. One succesfull incarnation of the ideas introduced
 The user interfaces now adopted by all the proof assistants that adopt a
 procedural proof language have been inspired by the CtCoq pioneering
 system~\cite{ctcoq}. One succesfull incarnation of the ideas introduced

-by CtCoq is the Proof General generic interface, that has set a sort of
+by CtCoq is the Proof General generic interface~\cite{proofgeneral},
+that has set a sort of

 standard way to interact with the system. Several procedural proof assistants
 have either adopted or cloned Proof General as their main user interface.
 \MATITA{} has also cloned the Proof General interface,
 standard way to interact with the system. Several procedural proof assistants
 have either adopted or cloned Proof General as their main user interface.
 \MATITA{} has also cloned the Proof General interface,


@@ -1205,51 +1206,38 @@ expression and the suffix \verb+_to_Prop+. In the above example,
  \end{center}
 \end{figure}
 
  \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. 
-
-\subsection{Patterns}
-
-\subsubsection{Direct manipulation of terms}
+\MATITA{} has a script based user interface (UI) for proof authoring,
+based on the paradigm already exploited by other widespread user
+interfaces for theorem provers like the Proof
+General~\cite{proofgeneral} generic interface.  We choosed not to
+build \MATITA{} UI over Proof General for two reasons. First because
+we had the need to integrate our rendering technologies --- mainly
+\GTKMATHVIEW{} --- based on XML markup languages whereas 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 would like \MATITA{} UI to be built on top of a
+state-of-the-art and widespread toolkit as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} UI.  As can
+be seen 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 \GTKMATHVIEW.  A distinguished part of the script (shaded
+in the screenshot) contains 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 over 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}.
+
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
+
+\subsection{Direct manipulation of terms}

 
 While terms are input as \TeX-like formulae in \MATITA, they're converted to a
 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
 
 While terms are input as \TeX-like formulae in \MATITA, they're converted to a
 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by


@@ -1289,38 +1277,42 @@ latter denotes an incomplete $\Pi$-binder. Once a (sub)term has been
 selected that way actions can be done on it like reductions or tactic
 applications.
 
 selected that way actions can be done on it like reductions or tactic
 applications.
 

+
+\subsection{Patterns}
+

 In our experience working with direct manipulation of terms is really
 In our experience working with direct manipulation of terms is really

-effective and faster than retyping them. Nonetheless we need a way to
-encode term selections in scripts so that they can be batch compiled
-by \MATITAC. In \MATITA{} \emph{patterns} implement that encoding,
-being patterns the textual representations of \GTKMATHVIEW{} semantic
-selections.  \NOTE{Zack:c'\`e scritto da qualche parte che l'utente
-non li deve necessariamente scrivere a mano, ma che pu\`o incollarli?
-Va scritto.}
+effective and is faster than typing the corresponding textual commands
+when they contain non-trivial terms. Nonetheless we need a way to
+represent term selections in scripts so that they can be batch
+compiled by \MATITAC.
+
+In \MATITA{} \emph{patterns} are such representation: each possible
+semantic selection in \GTKMATHVIEW{} can be represented as a textual
+pattern and batchly processed. Users can select using the GUI and then
+ask the system to paste the corresponding pattern in this script, but
+more often this process is transparent: once an action is performed on
+a selection, the corresponding textual command is computed and
+inserted in the script.

 
 \subsubsection{Pattern syntax}
 
 \subsubsection{Pattern syntax}

-A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
-$\NT{wanted}$.
-The former mocks-up a sequent, discharging unwanted subterms with $?$ and
-selecting the interesting parts with the placeholder $\%$. 
-The latter is a term that lives in the context of the placeholders.
-
-The concrete syntax is reported in table \ref{tab:pathsyn}
-\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
+
+Patterns are composed of two parts: \NT{sequent\_path} and
+\NT{wanted}; their concrete syntax is reported in table
+\ref{tab:pathsyn}.
+
+\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
+with $?$ and selecting the interesting parts with the placeholder
+$\%$.  \NT{wanted} is a term that lives in the context of the
+placeholders.
+
+Since there exists a bijection between sequent paths and visual
+selections, \MATITA{} uses only the \NT{sequent\_path} part to
+represent selections in scripts.  The \NT{wanted} part of the syntax
+is meant to help the users in writing concise and elegant patterns.
+

 \begin{table}
  \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
 \hrule
 \begin{table}
  \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
 \hrule

-% \[
-% \begin{array}{@{}rcll@{}}
-%   \NT{pattern} & 
-%     ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
-%   \NT{sequent\_path} & 
-%     ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
-%       [~\verb+\vdash+~\NT{multipath}~] & \\
-%   \NT{wanted} & ::= & \NT{term} & \\
-%   \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
-% \end{array}
-% \]

 \[
 \begin{array}{@{}rcll@{}}
   \NT{pattern} & 
 \[
 \begin{array}{@{}rcll@{}}
   \NT{pattern} & 


@@ -1335,13 +1327,13 @@ The concrete syntax is reported in table \ref{tab:pathsyn}
 \hrule
 \end{table}
 
 \hrule
 \end{table}
 

-\subsubsection{Pattern concepts}
-Patterns mimic the user's selection in two steps. The first one
-selects roots (subterms) of the sequent, using the
-$\NT{sequent\_path}$,  while the second 
-one searches the $\NT{wanted}$ term starting from these roots. Both are
-optional steps, and by convention the empty pattern selects the whole
-conclusion.
+\subsubsection{Pattern evaluation}
+
+Patterns are evaluated in two phases. The first selects roots
+(subterms) of the sequent, using the $\NT{sequent\_path}$,  while the
+second searches the $\NT{wanted}$ term starting from these roots.
+% Both are optional steps, and by convention the empty pattern selects
+% the whole conclusion.

 
 \begin{description}
 \item[Phase 1]
 
 \begin{description}
 \item[Phase 1]


@@ -1381,18 +1373,10 @@ conclusion.
 
 \end{description}
 
 
 \end{description}
 

-\noindent
-Since the first step is equipotent to the composition of the two
-steps, the system uses it to represent each visual selection.
-The second step is only meant for the
-experienced user that writes patterns by hand, since it really
-helps in writing concise patterns as we will see in the
-following examples.
-

 \subsubsection{Examples}
 \subsubsection{Examples}

-To explain how the first step works let's give an example. Consider
+To explain how the first phase works let's give an example. Consider

 you want to prove the uniqueness of the identity element $0$ for natural
 you want to prove the uniqueness of the identity element $0$ for natural

-sum, and that you can relay on the previously demonstrated left
+sum, and that you can rely on the previously demonstrated left

 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
 Typing
 \begin{grafite}
 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
 Typing
 \begin{grafite}