added klocs sums and heading "0." where missing

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 82f3256e6e8dc8042966c7f2d41f646efdafb425..192117af50dd9c14139cddad54e7adf7c11301a4 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -298,9 +298,9 @@ allow other developers to quickly understand our code and contribute.
 \section{Architecture}
 \label{architettura}
 
-\begin{figure}[ht]
+\begin{figure}[!ht]
  \begin{center}
-  \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
+  \includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters}
   \caption{\MATITA{} components}
   \label{fig:libraries}
  \end{center}
@@ -700,10 +700,9 @@ in its script based authoring interface.
 
 In the remaining part of the paper we focus on the user view of \MATITA{}.
 This section is devoted to the aspects of the tool that arise from the
-document centric approach to the library. Sect.~\ref{authoring} describes
+document centric approach to the library. Sect.~\ref{sec:authoring} describes
 the peculiarities of the authoring interface.
 
-
 The library of \MATITA{} comprises mathematical concepts (theorems,
 axioms, definitions) and notation. The concepts are authored sequentially
 using scripts that are (ordered) sequences of procedural commands.
@@ -712,7 +711,7 @@ The only relation implicitly kept between the notions are the logical,
 acyclic dependencies among them. This way the library forms a global (and
 distributed) hypertext. Several useful operations can be implemented on the
 library only, regardless of the scripts. Examples of such operations
-implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:index});
+implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:indexing});
 disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
 automatic proof searching (see Sect.~\ref{sec:automation}).
 
@@ -730,7 +729,7 @@ fully restored.
 To implement the proposed versioning system on top of a standard one
 it is necessary to implement \emph{invalidation} first. Invalidation
 is the operation that locates and removes from the library all the concepts
-that depend on a given one. As described in Sect.~\ref{sec:...}, removing
+that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
 a concept from the library also involves deleting its metadata from the
 database.
 
@@ -740,7 +739,7 @@ development, you are free to change and invalidate part of the library
 without branching. Invalidation is still necessary to avoid using a
 concept that is no longer valid.
 So far, in \MATITA{} we address only this non collaborative scenario
-(see Sect.~\ref{sec:decompilazione}). Collaborative development and versioning
+(see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
 is still under design.
 
 Scripts are not seen as constituents of the library. They are not published
@@ -758,6 +757,7 @@ of \MATITA{} related to library management and exploitation.
 
 
 \subsection{Indexing and searching}
+\label{sec:indexing}
 
 \subsection{Disambiguation}
 \label{sec:disambiguation}
@@ -1127,6 +1127,7 @@ no risk of introducing dangling references since the \MATITA{} user
 interface inhibit undoing a step which is not the last executed.
 
 \subsection{Automation}
+\label{sec:automation}
 
 \subsection{Naming convention}
 A minor but not entirely negligible aspect of \MATITA{} is that of
@@ -1194,6 +1195,7 @@ expression and the suffix \verb+_to_Prop+. In the above example,
 \verb+eqb_to_Prop+ is accepted. 
 
 \section{The authoring interface}
+\label{sec:authoring}
 
 \begin{figure}[t]
  \begin{center}