X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=97e8c2f431f435ec82df87ae4ab8d0cbd3d7f8f9;hb=3af56c5a48f7cad33fd701e0061fe143e0e2a7c5;hp=21ed483ad157bc64de0abe11bdf4b100766d3908;hpb=faafe87ce2f7906abc4638cd8f69d1b82dece371;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 21ed483ad..97e8c2f43 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -43,6 +43,8 @@ type resolve_result =
   | Exception of exn
   | Resolved of string
 
+type logger_callback = HelmLogger.html_tag -> unit
+
 let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
 
 let (index_line_sep_RE, index_sep_RE, trailing_types_RE,
@@ -76,7 +78,7 @@ let map_of_uri = function
   | uri when is_xsl_uri uri -> Lazy.force xsl_map
   | uri -> raise (Unresolvable_URI uri)
 
-let update_from_server logmsg server_url = (* use global maps *)
+let update_from_server logger server_url = (* use global maps *)
   debug_print ("Updating information from " ^ server_url);
   let xml_url_of_uri = function
       (* TODO missing sanity checks on server_url, e.g. it can contains $1 *)
@@ -95,7 +97,7 @@ let update_from_server logmsg server_url = (* use global maps *)
         Pcre.replace ~rex:heading_rdf_theory_RE ~templ:server_url uri
     | uri -> raise (Invalid_URI uri)
   in
-  let log = ref (`T ("Processing server: " ^ server_url) :: logmsg) in
+  logger (`T ("Processing server: " ^ server_url));
   let (xml_index, rdf_index, xsl_index) =
     (* TODO keeps index in memory, is better to keep them on temp files? *)
     (http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xml_index)),
@@ -106,7 +108,7 @@ let update_from_server logmsg server_url = (* use global maps *)
     debug_print (sprintf "Warning: useless server %s" server_url);
   (match xml_index with
   | Some xml_index ->
-      (log := `T "Updating XML db ...<br />" :: !log;
+      logger (`T "Updating XML db ...<br />");
       List.iter
         (function
           | l when is_blank_line l -> ()  (* skip blank and commented lines *)
@@ -121,15 +123,15 @@ let update_from_server logmsg server_url = (* use global maps *)
                    assert (is_cic_uri uri || is_nuprl_uri uri) ;
                    (map_of_uri uri)#replace
                     uri ((xml_url_of_uri uri) ^ ".xml")
-                | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log)
+                | _ -> logger (`T ("Ignoring invalid line: '" ^ l)))
               with Invalid_URI uri ->
-                log := `T ("Ignoring invalid XML URI: '" ^ l) :: !log))
+                logger (`T ("Ignoring invalid XML URI: '" ^ l))))
         (Pcre.split ~rex:index_sep_RE xml_index); (* xml_index lines *)
-      log := `T "All done" :: !log)
+      logger (`T "All done")
   | None -> ());
   (match rdf_index with
   | Some rdf_index ->
-      (log := `T "Updating RDF db ..." :: !log;
+      logger (`T "Updating RDF db ...");
       List.iter
         (fun l ->
           try
@@ -140,38 +142,32 @@ let update_from_server logmsg server_url = (* use global maps *)
             | [uri] ->
                 (Lazy.force rdf_map) # replace uri
                   ((rdf_url_of_uri uri) ^ ".xml")
-            | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log)
+            | _ -> logger (`T ("Ignoring invalid line: '" ^ l)))
           with Invalid_URI uri ->
-            log := `T ("Ignoring invalid RDF URI: '" ^ l) :: !log)
+            logger (`T ("Ignoring invalid RDF URI: '" ^ l)))
         (Pcre.split ~rex:index_sep_RE rdf_index); (* rdf_index lines *)
-      log := `T "All done" :: !log)
+      logger (`T "All done")
   | None -> ());
   (match xsl_index with
   | Some xsl_index ->
-      (log := `T "Updating XSLT db ..." :: !log;
+      logger (`T "Updating XSLT db ...");
       List.iter
         (fun l -> (Lazy.force xsl_map) # replace l (server_url ^ "/" ^ l))
         (Pcre.split ~rex:index_sep_RE xsl_index);
-      log := `T "All done" :: !log)
+      logger (`T "All done")
   | None -> ());
-  debug_print "done with this server";
-  !log
+  debug_print "done with this server"
 
-let update_from_all_servers () =  (* use global maps *)
+let update_from_all_servers logger () =  (* use global maps *)
   clear_maps ();
-  let log =
-    List.fold_left
-      update_from_server
-      []  (* initial logmsg: empty *)
-        (* reverse order: 1st server is the most important one *)
-      (List.map snd (List.rev (Http_getter_env.servers ())))
-  in
-  sync_maps ();
-  `Msg (`L (List.rev log))
+  List.iter
+    (update_from_server logger)
+      (* reverse order: 1st server is the most important one *)
+    (List.map snd (List.rev (Http_getter_env.servers ())));
+  sync_maps ()
 
-let update_from_one_server server_url =
-  let log = update_from_server [] server_url in
-  `Msg (`L (List.rev log))
+let update_from_one_server ?(logger = fun _ -> ()) server_url =
+  update_from_server logger server_url
 
 let temp_file_of_uri uri =
   let flat_string s s' c =
@@ -198,8 +194,8 @@ let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote"
 let getdtd_remote ~patch_dtd uri = not_implemented "getdtd_remote"
 let clean_cache_remote () = not_implemented "clean_cache_remote"
 let list_servers_remote () = not_implemented "list_servers_remote"
-let add_server_remote ~position name = not_implemented "add_server_remote"
-let remove_server_remote position = not_implemented "remove_server_remote"
+let add_server_remote ~logger ~position name = not_implemented "add_server_remote"
+let remove_server_remote ~logger position = not_implemented "remove_server_remote"
 let getalluris_remote () = not_implemented "getalluris_remote"
 let getallrdfuris_remote () = not_implemented "getallrdfuris_remote"
 let ls_remote lsuri = not_implemented "ls_remote"
@@ -229,9 +225,9 @@ let register_remote ~uri ~url =
 let register_remote ~uri ~url =
   ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
 
-let update_remote () =
+let update_remote logger  () =
   let answer = ClientHTTP.get (getter_url () ^ "update") in
-  `Msg (`T answer)
+  logger (`T answer)
 
 let getxml_remote ~format ~patch_dtd uri =
  ClientHTTP.get_and_save_to_tmp
@@ -259,11 +255,11 @@ let register ~uri ~url =
   else
     (map_of_uri uri)#add uri url
 
-let update () =
+let update ?(logger = fun _ -> ()) () =
   if remote () then
-    update_remote ()
+    update_remote logger ()
   else
-    update_from_all_servers ()
+    update_from_all_servers logger ()
 
 let getxml ?(format = Enc_normal) ?(patch_dtd = true) uri =
   if remote () then
@@ -311,23 +307,25 @@ let list_servers () =
   else
     Http_getter_env.servers ()
 
-let add_server ?(position = 0) name =
+let add_server ?(logger = fun _ -> ()) ?(position = 0) name =
   if remote () then
-    add_server_remote ~position name
+    add_server_remote ~logger ~position name
   else begin
     if position = 0 then begin
       Http_getter_env.add_server ~position:0 name;
-      update_from_one_server name (* quick update (new server only) *)
+      update_from_one_server ~logger name (* quick update (new server only) *)
     end else if position > 0 then begin
       Http_getter_env.add_server ~position name;
-      update ()
-    end else  (* already checked bt parse_position *)
+      update ~logger ()
+    end else  (* already checked by parse_position *)
       assert false
   end
 
-let remove_server position =
+let has_server position = List.mem_assoc position (Http_getter_env.servers ())
+
+let remove_server ?(logger = fun _ -> ()) position =
   if remote () then
-    remove_server_remote ()
+    remove_server_remote ~logger ()
   else begin
     let server_name =
       try
@@ -336,7 +334,7 @@ let remove_server position =
         raise (Invalid_argument (sprintf "no server with position %d" position))
     in
     Http_getter_env.remove_server position;
-    update ()
+    update ~logger ()
   end
 
 let return_uris map filter =