X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=0f20792d72bf634e7ced93d3ec172f262753e839;hb=7668522147126e620258e6d22c16a2b0fa56feb4;hp=807eecb5299df03d7f4611b7cf4c7f0e4781cfac;hpb=1145c5ea2e31055388f5f02c6382429a11fd5dd9;p=helm.git diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 807eecb52..0f20792d7 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -30,7 +30,6 @@ open Printf open Http_getter_common open Http_getter_misc -open Http_getter_debugger open Http_getter_types exception Not_implemented of string @@ -45,6 +44,8 @@ type resolve_result = type logger_callback = HelmLogger.html_tag -> unit +let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag) + let not_implemented s = raise (Not_implemented ("Http_getter." ^ s)) let (index_line_sep_RE, index_sep_RE, trailing_types_RE, @@ -79,7 +80,7 @@ let map_of_uri = function | uri -> raise (Unresolvable_URI uri) let update_from_server logger server_url = (* use global maps *) - debug_print ("Updating information from " ^ server_url); + Http_getter_logger.log ("Updating information from " ^ server_url); let xml_url_of_uri = function (* TODO missing sanity checks on server_url, e.g. it can contains $1 *) | uri when (Pcre.pmatch ~rex:heading_cic_RE uri) -> @@ -106,11 +107,11 @@ let update_from_server logger server_url = (* use global maps *) http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xsl_index))) in if (xml_index = None && rdf_index = None && xsl_index = None) then - debug_print (sprintf "Warning: useless server %s" server_url); + Http_getter_logger.log (sprintf "Warning: useless server %s" server_url); (match xml_index with | Some xml_index -> - logger (`T "Updating XML db ..."); - logger `BR; + logger (`T "- Updating XML db ..."); +(* logger `BR; *) List.iter (function | l when is_blank_line l -> () (* skip blank and commented lines *) @@ -137,8 +138,8 @@ let update_from_server logger server_url = (* use global maps *) | None -> ()); (match rdf_index with | Some rdf_index -> - logger (`T "Updating RDF db ..."); - logger `BR; + logger (`T "- Updating RDF db ..."); +(* logger `BR; *) List.iter (fun l -> try @@ -161,15 +162,15 @@ let update_from_server logger server_url = (* use global maps *) | None -> ()); (match xsl_index with | Some xsl_index -> - logger (`T "Updating XSLT db ..."); - logger `BR; + logger (`T "- Updating XSLT db ..."); +(* logger `BR; *) List.iter (fun l -> (Lazy.force xsl_map) # replace l (server_url ^ "/" ^ l)) (Pcre.split ~rex:index_sep_RE xsl_index); logger (`T "All done"); logger `BR | None -> ()); - debug_print "done with this server" + Http_getter_logger.log "done with this server" let update_from_all_servers logger () = (* use global maps *) clear_maps ();