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
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.
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.