From 460802c49902d1225b37ac6cd6f5aa599aa5ecd8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Jan 2006 10:12:42 +0000 Subject: [PATCH] uniformed (G|g)etter with \GETTER --- helm/papers/matita/matita2.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 3f3334403..4dbf40cae 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -332,9 +332,9 @@ be satisfied by linking the \component{} in the same executable. For those \components{} whose functionalities are also provided by the aforementioned Web services, it is also possible to link stub code that forwards the request to a remote Web service. For instance, the Getter -is just a wrapper to the \texttt{getter} \component{} that allows the +is just a wrapper to the \GETTER \component{} that allows the \component{} to be used as a Web service. \MATITA{} can directly link the code -of the \texttt{getter} \component, or it can use a stub library with the same +of the \GETTER \component, or it can use a stub library with the same API that forwards every request to the Getter. To better understand the architecture of \MATITA{} and the role of each @@ -369,11 +369,11 @@ content level terms; presentation level terms. Terms may reference other mathematical notions in the library. One commitment of our project is that the library should be physically - distributed. The \texttt{getter} \component{} manages the distribution, + distributed. The \GETTER \component{} manages the distribution, providing a mapping from logical names (URIs) to the physical location of a notion (an URL). The \texttt{urimanager} \component{} provides the URI data type and several utility functions over URIs. The - \texttt{cic\_proof\_checking} \component{} calls the \texttt{getter} + \texttt{cic\_proof\_checking} \component{} calls the \GETTER \component{} every time it needs to retrieve the definition of a mathematical notion referenced by a term that is being type-checked. @@ -709,7 +709,7 @@ classical filesystem and a relational database. The former is used to store the XML encoding of the objects defined in the script, the disambiguation aliases and the interpretation and notational convention defined, while the latter is used to store all the metadata needed by -\WHELP{}. In addition the \emph{getter} component +\WHELP{}. In addition the \GETTER component should be updated with the the new mapping between the logical URI and the physical path of objects. -- 2.39.5