From f0d65b5632900e307cf918d51094e9d69350501c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 25 Nov 2005 12:09:18 +0000 Subject: [PATCH] ... --- helm/papers/matita/matita2.tex | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 44e301a79..f1699bc2f 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -409,6 +409,19 @@ translation is an ambiguous language and the user is free to associate to every content level term several different interpretations (as a partially specified term). +The \MATITA{} proof assistant and the \WHELP{} search engine are both linked +against the \texttt{cic\_disambiguation} and \texttt{content\_pres} libraries +since they provide an interface to the user. In both cases the formulae +written by the user are parsed using the \texttt{content\_pres} library and +then disambiguated using the \texttt{cic\_disambiguation} library. + +The \UWOBO{} Web service wraps the \texttt{content\_pres} library, +providing a rendering service for the documents in the distributed library. +To render a document given its URI, \UWOBO{} retrieves it using the +\GETTER{} obtaining a document with fully specified terms. Then it translates +it to the presentation level passing through the content level. Finally +it returns the result document to be rendered by the user's browser. + \hrule At the bottom of the DAG we have a few libraries (\texttt{extlib}, -- 2.39.2