X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_cache%2FcicCache.ml;h=b4ae4fbec3261fe31109778e2896f17fe10fc77f;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=29d6a9a2fb445fd3a34164c7645a854773e8ac56;hpb=768205685b87c4ae4c062b3bc9fa5e51951b2608;p=helm.git diff --git a/helm/ocaml/cic_cache/cicCache.ml b/helm/ocaml/cic_cache/cicCache.ml index 29d6a9a2f..b4ae4fbec 100644 --- a/helm/ocaml/cic_cache/cicCache.ml +++ b/helm/ocaml/cic_cache/cicCache.ml @@ -36,9 +36,8 @@ (******************************************************************************) let get_annobj uri = - let module G = Getter in let module U = UriManager in - let cicfilename = G.getxml (U.cicuri_of_uri uri) in + let cicfilename = Http_getter.getxml' (U.cicuri_of_uri uri) in match (U.bodyuri_of_uri uri) with None -> let annobj = CicParser.annobj_of_xml cicfilename None in @@ -47,11 +46,11 @@ let get_annobj uri = | Some bodyuri -> let cicbodyfilename = try - ignore (Getter.resolve bodyuri) ; + ignore (Http_getter.resolve' bodyuri) ; (* The body exists ==> it is not an axiom *) - Some (Getter.getxml bodyuri) + Some (Http_getter.getxml' bodyuri) with - Getter.Unresolved -> + Http_getter_types.Unresolvable_URI _ -> (* The body does not exist ==> we consider it an axiom *) None in @@ -64,9 +63,8 @@ let get_annobj uri = ;; let get_obj uri = - let module G = Getter in let module U = UriManager in - let cicfilename = G.getxml (U.cicuri_of_uri uri) in + let cicfilename = Http_getter.getxml' (U.cicuri_of_uri uri) in match (U.bodyuri_of_uri uri) with None -> let obj = CicParser.obj_of_xml cicfilename None in @@ -75,11 +73,10 @@ let get_obj uri = | Some bodyuri -> let cicbodyfilename = try - ignore (Getter.resolve bodyuri) ; + ignore (Http_getter.resolve' bodyuri) ; (* The body exists ==> it is not an axiom *) - Some (Getter.getxml bodyuri) - with - Getter.Unresolved -> + Some (Http_getter.getxml' bodyuri) + with Http_getter_types.Unresolvable_URI _ -> (* The body does not exist ==> we consider it an axiom *) None in