X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=7fee306a605d169763849e2c55cea21851810776;hb=eac74259f5a0aaa8056791876284c897a6827c24;hp=35a19db82bb4f5fc06afe990421085d09e147e81;hpb=ae1f66ceadc14c7d0824bb375c5af175b15f083c;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 35a19db82..7fee306a6 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -230,7 +230,8 @@ let resolve_remote uri =
           res := Exception (Unresolvable_URI uri)
       | Pxp_types.E_start_tag ("not_found",[],_,_) ->
           res := Exception (Key_not_found uri)
-      | Pxp_types.E_start_tag _ -> res := Exception UnexpectedGetterOutput
+      | Pxp_types.E_start_tag (x,_,_,_) -> 
+	  res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
    | Unknown -> raise UnexpectedGetterOutput
@@ -263,8 +264,17 @@ let resolve uri =
   if remote () then
     resolve_remote uri
   else
-    (map_of_uri uri)#resolve uri
-
+    
+    (**** FIXME ******)
+    if is_cic_uri uri && Pcre.pmatch ~pat:"\\.univ$" uri then
+      begin
+	prerr_endline "!!! E' in ~tassi !!!";
+	"file:///home/tassi/mylib" ^ 
+	(String.sub uri 4 ((String.length uri) - 4)) ^ ".xml.gz"
+      end
+    else
+      (map_of_uri uri)#resolve uri
+	
 let register ~uri ~url =
   if remote () then
     register_remote ~uri ~url
@@ -275,7 +285,9 @@ let unregister uri =
   if remote () then
     unregister_remote uri
   else
-    (map_of_uri uri)#remove uri
+    try
+      (map_of_uri uri)#remove uri
+    with Key_not_found _ -> ()
 
 let update ?(logger = fun _ -> ()) () =
   if remote () then
@@ -287,7 +299,9 @@ let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
   if remote () then
     getxml_remote ~format ~patch_dtd uri
   else begin
+    Http_getter_logger.log ~level:2 ("getxml: " ^ uri);
     let url = resolve uri in
+    Http_getter_logger.log ~level:2 ("resolved_uri: " ^ url) ;
     let (fname, outchan) = temp_file_of_uri uri in
     Http_getter_cache.respond_xml ~via_http:false ~enc:format ~patch:patch_dtd
       ~uri ~url outchan;
@@ -299,6 +313,7 @@ let getxslt ?(patch_dtd = true) uri =
   if remote () then
     getxslt_remote ~patch_dtd uri
   else begin
+    
     let url = resolve uri in
     let (fname, outchan) = temp_file_of_uri uri in
     Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan;
@@ -527,4 +542,10 @@ prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
 let getxml' uri = getxml (UriManager.string_of_uri uri)
 let resolve' uri = resolve (UriManager.string_of_uri uri)
 let register' uri url = register ~uri:(UriManager.string_of_uri uri) ~url
+let init () =
+  Http_getter_logger.set_log_level
+    (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+  Http_getter_logger.set_log_file
+    (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+  Http_getter_env.reload ()