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}
 
 \section{Architecture}
 \label{architettura}
 

-\begin{figure}[ht]
+\begin{figure}[!ht]

  \begin{center}
  \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}
   \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
 
 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 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.
 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
 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}).
 
 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
 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.
 
 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
 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
 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}
 
 
 \subsection{Indexing and searching}

+\label{sec:indexing}

 
 \subsection{Disambiguation}
 \label{sec:disambiguation}
 
 \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}
 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
 
 \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}
 \verb+eqb_to_Prop+ is accepted. 
 
 \section{The authoring interface}

+\label{sec:authoring}

 
 \begin{figure}[t]
  \begin{center}
 
 \begin{figure}[t]
  \begin{center}