X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_env.ml;h=a7fe6be91d14701a69e0a150b31488a370e9c870;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=3264d6c65c33c546f6acae91acf0a20239627b39;hpb=faafe87ce2f7906abc4638cd8f69d1b82dece371;p=helm.git diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml index 3264d6c65..a7fe6be91 100644 --- a/helm/ocaml/getter/http_getter_env.ml +++ b/helm/ocaml/getter/http_getter_env.ml @@ -47,7 +47,10 @@ let cic_dir = lazy (Helm_registry.get "getter.cic_dir") let nuprl_dir = lazy (Helm_registry.get "getter.nuprl_dir") let rdf_dir = lazy (Helm_registry.get "getter.rdf_dir") let dtd_dir = lazy (Helm_registry.get "getter.dtd_dir") -let dtd_base_url = lazy (Helm_registry.get "getter.dtd_base_url") +let dtd_base_urls = lazy ( + let rex = Pcre.regexp "/*$" in + let raw_urls = Helm_registry.get_string_list "getter.dtd_base_urls" in + List.map (Pcre.replace ~rex) raw_urls) let port = lazy (Helm_registry.get_int "getter.port") let _servers = ref None @@ -92,8 +95,8 @@ let my_own_url = let cache_mode = lazy (match String.lowercase (Helm_registry.get "getter.cache_mode") with - | "normal" -> Enc_normal - | "gz" -> Enc_gzipped + | "normal" -> `Normal + | "gz" -> `Gzipped | mode -> failwith ("Invalid cache mode: " ^ mode)) let reload () = reload_servers () @@ -117,10 +120,12 @@ servers_file:\t%s host:\t\t%s port:\t\t%d my_own_url:\t%s -dtd_base_url:\t%s +dtd_base_urls:\t%s cache_mode:\t%s servers: \t%s +log_file:\t%s +log_level:\t%d " version (Lazy.force cic_dbm) (Lazy.force nuprl_dbm) (Lazy.force rdf_dbm) (Lazy.force xsl_dbm) (Lazy.force xml_index) @@ -128,11 +133,15 @@ servers: (Lazy.force nuprl_dir) (Lazy.force rdf_dir) (Lazy.force dtd_dir) (Lazy.force servers_file) (Lazy.force host) (Lazy.force port) (Lazy.force my_own_url) - (Lazy.force dtd_base_url) - (match Lazy.force cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped") + (String.concat " " (Lazy.force dtd_base_urls)) + (match Lazy.force cache_mode with + | `Normal -> "Normal" + | `Gzipped -> "GZipped") (String.concat "\n\t" (* (position * server) list *) (List.map (fun (pos, server) -> sprintf "%3d: %s" pos server) (servers ()))) + (match Http_getter_logger.get_log_file () with None -> "None" | Some f -> f) + (Http_getter_logger.get_log_level ()) let add_server ?position url = let new_servers =