From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Feb 2005 09:28:07 +0000 (+0000)
Subject: - added init method
X-Git-Tag: V_0_1_0~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29af46301fcf532dbebd3ef0eef666adc7e6ccf4;p=helm.git

- added init method
- added default values for loglevel and logfile
---

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 84b2277a1..7fee306a6 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -285,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
@@ -297,9 +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 ("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;
@@ -540,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 ()
 
diff --git a/helm/ocaml/getter/http_getter.mli b/helm/ocaml/getter/http_getter.mli
index f0b32b384..c7a2c5c2a 100644
--- a/helm/ocaml/getter/http_getter.mli
+++ b/helm/ocaml/getter/http_getter.mli
@@ -45,7 +45,7 @@ val resolve: string -> string (* uri -> url *)
   (** @raise Http_getter_types.Key_already_in _ *)
 val register: uri:string -> url:string -> unit
 
-  (** @raise Http_getter_types.Key_not_found _ *)
+  (** does not fail if given uri does not exist *)
 val unregister: string -> unit
 
 val update: ?logger:logger_callback -> unit -> unit
@@ -73,4 +73,5 @@ val register' : UriManager.uri -> string -> unit
 val close_maps: unit -> unit
 val update_from_one_server: ?logger:logger_callback -> string -> unit
 val has_server: int -> bool (* does a server with a given position exists? *)
+val init: unit -> unit