X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_env.ml;h=575207057b60a4d85a429fae90d5d0a9f584913a;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;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..575207057 100644 --- a/helm/ocaml/getter/http_getter_env.ml +++ b/helm/ocaml/getter/http_getter_env.ml @@ -35,20 +35,39 @@ open Http_getter_types let version = Http_getter_const.version -let servers_file = lazy (Helm_registry.get "getter.servers_file") -let cic_dbm = lazy (Helm_registry.get "getter.cic_dbm") -let nuprl_dbm = lazy (Helm_registry.get "getter.nuprl_dbm") -let rdf_dbm = lazy (Helm_registry.get "getter.rdf_dbm") -let xsl_dbm = lazy (Helm_registry.get "getter.xsl_dbm") -let xml_index = lazy (Helm_registry.get "getter.xml_indexname") -let rdf_index = lazy (Helm_registry.get "getter.rdf_indexname") -let xsl_index = lazy (Helm_registry.get "getter.xsl_indexname") -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 servers_file = lazy ( + Helm_registry.get_opt Helm_registry.get "getter.servers_file") +let cic_dbm = lazy (Helm_registry.get "getter.maps_dir" ^ "/cic_db") +let cic_dbm_real = lazy (Helm_registry.get "getter.maps_dir" ^ "/cic_db.pag") +let nuprl_dbm = lazy (Helm_registry.get "getter.maps_dir" ^ "/nuprl_db") +let rdf_dbm = lazy (Helm_registry.get "getter.maps_dir" ^ "/rdf_db") +let xsl_dbm = lazy (Helm_registry.get "getter.maps_dir" ^ "/xsl_db") +let dump_file = lazy (Helm_registry.get "getter.maps_dir" ^ + "/cic_db_tree.dump") +let prefetch = lazy (Helm_registry.get_bool "getter.prefetch") +let xml_index = lazy ( + Helm_registry.get_opt_default Helm_registry.get "index.txt" + "getter.xml_indexname") +let rdf_index = lazy ( + Helm_registry.get_opt_default Helm_registry.get "rdf_index.txt" + "getter.rdf_indexname") +let xsl_index = lazy ( + Helm_registry.get_opt_default Helm_registry.get "xslt_index.txt" + "getter.xsl_indexname") +let cic_dir = lazy (Helm_registry.get "getter.cache_dir" ^ "/cic") +let nuprl_dir = lazy (Helm_registry.get "getter.cache_dir" ^ "/nuprl") +let rdf_dir = lazy (Helm_registry.get "getter.cache_dir" ^ "/rdf") let dtd_dir = lazy (Helm_registry.get "getter.dtd_dir") -let dtd_base_url = lazy (Helm_registry.get "getter.dtd_base_url") -let port = lazy (Helm_registry.get_int "getter.port") +let dtd_base_urls = lazy ( + let rex = Pcre.regexp "/*$" in + let raw_urls = + Helm_registry.get_opt_default Helm_registry.get_string_list + ["http://helm.cs.unibo.it/dtd"; "http://mowgli.cs.unibo.it/dtd"] + "getter.dtd_base_urls" + in + List.map (Pcre.replace ~rex) raw_urls) +let port = lazy ( + Helm_registry.get_opt_default Helm_registry.get_int 58081 "getter.port") let _servers = ref None @@ -59,22 +78,30 @@ let servers = | Some servers -> servers) let load_servers () = - let pos = ref (-1) in - List.rev (Http_getter_misc.fold_file - (fun line servers -> - if Http_getter_misc.is_blank_line line then - servers - else - (incr pos; (!pos, line) :: servers)) - [] - (Lazy.force servers_file)) + let pos = ref ~-1 in + match Lazy.force servers_file with + | None -> + List.map (fun s -> incr pos; (!pos, s)) + (Helm_registry.get_string_list "getter.servers") + | Some servers_file -> + List.rev (Http_getter_misc.fold_file + (fun line servers -> + if Http_getter_misc.is_blank_line line then + servers + else + (incr pos; (!pos, line) :: servers)) + [] + servers_file) let reload_servers () = _servers := Some (load_servers ()) let save_servers () = - let oc = open_out (Lazy.force servers_file) in - List.iter (fun (_,server) -> output_string oc (server ^ "\n")) - (servers ()); + match Lazy.force servers_file with + | None -> () + | Some servers_file -> + let oc = open_out servers_file in + List.iter (fun (_,server) -> output_string oc (server ^ "\n")) + (servers ()); close_out oc let host = @@ -91,9 +118,12 @@ let my_own_url = let cache_mode = lazy - (match String.lowercase (Helm_registry.get "getter.cache_mode") with - | "normal" -> Enc_normal - | "gz" -> Enc_gzipped + (let mode_string = + Helm_registry.get_opt_default Helm_registry.get "gz" "getter.cache_mode" + in + match String.lowercase mode_string with + | "normal" -> `Normal + | "gz" -> `Gzipped | mode -> failwith ("Invalid cache mode: " ^ mode)) let reload () = reload_servers () @@ -113,26 +143,38 @@ cic_dir:\t%s nuprl_dir:\t%s rdf_dir:\t%s dtd_dir:\t%s +dump_file:\t%s +prefetch:\t%b 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) (Lazy.force rdf_index) (Lazy.force xsl_index) (Lazy.force cic_dir) (Lazy.force nuprl_dir) (Lazy.force rdf_dir) - (Lazy.force dtd_dir) (Lazy.force servers_file) (Lazy.force host) + (Lazy.force dtd_dir) (Lazy.force dump_file) (Lazy.force prefetch) + (match Lazy.force servers_file with + | None -> "no servers file" + | Some servers_file -> 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 =