rebuilt against ocaml 3.08.3

[helm.git] / helm / ocaml / getter / http_getter.ml

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 539fa90a700570b6be85179b8e42513c903c5e8e..f7ca2388c89b9653d04f8087ac4d021fc8d1e966 100644 (file)
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -77,7 +77,7 @@ let map_of_uri = function
   | uri when is_nuprl_uri uri -> Lazy.force nuprl_map
   | uri when is_rdf_uri uri -> Lazy.force rdf_map
   | uri when is_xsl_uri uri -> Lazy.force xsl_map
-  | uri -> prerr_endline "BBBBB";raise (Unresolvable_URI uri)
+  | uri -> raise (Unresolvable_URI uri)
 
 let update_from_server logger server_url = (* use global maps *)
   Http_getter_logger.log ("Updating information from " ^ server_url);
@@ -231,16 +231,11 @@ let resolve_remote uri =
       | Pxp_types.E_start_tag ("not_found",[],_,_) ->
           res := Exception (Key_not_found uri)
       | Pxp_types.E_start_tag (x,_,_,_) -> 
-         prerr_endline ("UnexpectedGetterOutput: "^x);
          res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
-   | Unknown -> 
-       prerr_endline ("UnexpectedGetterOutput: Unknown!");
-       raise UnexpectedGetterOutput
-   | Exception e -> 
-       prerr_endline ("Exception   : ??????");
-       raise e
+   | Unknown -> raise UnexpectedGetterOutput
+   | Exception e -> raise e
    | Resolved url -> url
 
 let register_remote ~uri ~url =
@@ -269,16 +264,7 @@ let resolve uri =
   if remote () then
     resolve_remote uri
   else
-    
-    (**** 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
+    (map_of_uri uri)#resolve uri
        
 let register ~uri ~url =
   if remote () then
@@ -290,7 +276,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
@@ -302,9 +290,9 @@ let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
   if remote () then
     getxml_remote ~format ~patch_dtd uri
   else begin
-Http_getter_logger.log ("GETXML: " ^ uri);
+    Http_getter_logger.log ~level:2 ("getxml: " ^ uri);
     let url = resolve uri in
-Http_getter_logger.log ("RESOLVED_URI: " ^ url) ;
+    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;
@@ -387,8 +375,8 @@ let getalluris () =
     getalluris_remote ()
   else
     let filter uri =
-      (Pcre.pmatch ~rex:heading_cic_RE uri) &&
-      not (Pcre.pmatch ~rex:trailing_types_RE uri)
+      (Pcre.pmatch ~rex:heading_cic_RE uri)
+(*       && not (Pcre.pmatch ~rex:trailing_types_RE uri) *)
     in
     return_uris (Lazy.force cic_map) filter
 
@@ -503,9 +491,6 @@ let ls =
                  let dir =
                   "theory" ^ String.sub !dir_found 3
                    (String.length !dir_found - 3) ^ ".theory" in
-(*
-prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
-*)
                  if not (List.mem dir !valid_candidates) then
                  valid_candidates := dir::!valid_candidates
                end
@@ -518,10 +503,6 @@ prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
              then
               (index_not_generated_yet := false ;
                store_obj "index.theory"));
-(*
-prerr_endline ("@@@ " ^ String.concat " " !valid_candidates);
-prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
-*)
       List.iter
        (fun (uri,localpart) ->
          if not (List.mem uri !valid_candidates) then
@@ -545,4 +526,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 ()