]> matita.cs.unibo.it Git - helm.git/commitdiff
uniformed (G|g)etter with \GETTER
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 23 Jan 2006 10:12:42 +0000 (10:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 23 Jan 2006 10:12:42 +0000 (10:12 +0000)
helm/papers/matita/matita2.tex

index 3f333440334aeed9c7fe542534e73c099f5692df..4dbf40cae059a48ad3acf3f8a8890623f94dbdb6 100644 (file)
@@ -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.