X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_env.ml;h=1fa159a3cd73c2717a721b73db371e6f9593f62c;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=a7fe6be91d14701a69e0a150b31488a370e9c870;hpb=7c2045fe89bee49c3eaf04b92fd05e577174dcb9;p=helm.git

diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml
index a7fe6be91..1fa159a3c 100644
--- a/helm/ocaml/getter/http_getter_env.ml
+++ b/helm/ocaml/getter/http_getter_env.ml
@@ -27,31 +27,46 @@
  *)
 
 open Printf
-open Pxp_document
-open Pxp_types
-open Pxp_yacc
 
 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.string "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.string ~default:"index.txt"
+    "getter.xml_indexname")
+let rdf_index       = lazy (
+  Helm_registry.get_opt_default Helm_registry.string ~default:"rdf_index.txt"
+    "getter.rdf_indexname")
+let xsl_index       = lazy (
+  Helm_registry.get_opt_default Helm_registry.string ~default:"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_urls   = lazy (
   let rex = Pcre.regexp "/*$" in
-  let raw_urls = Helm_registry.get_string_list "getter.dtd_base_urls" in
+  let raw_urls =
+    match
+      Helm_registry.get_list Helm_registry.string "getter.dtd_base_urls"
+    with
+    | [] -> ["http://helm.cs.unibo.it/dtd"; "http://mowgli.cs.unibo.it/dtd"]
+    | urls -> urls
+  in
   List.map (Pcre.replace ~rex) raw_urls)
-let port            = lazy (Helm_registry.get_int "getter.port")
+let port            = lazy (
+  Helm_registry.get_opt_default Helm_registry.int ~default:58081 "getter.port")
 
 let _servers = ref None
 
@@ -62,22 +77,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_list Helm_registry.string "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 =
@@ -94,7 +117,11 @@ let my_own_url =
 
 let cache_mode =
   lazy
-    (match String.lowercase (Helm_registry.get "getter.cache_mode") with
+    (let mode_string =
+      Helm_registry.get_opt_default Helm_registry.string ~default:"gz"
+        "getter.cache_mode"
+    in
+    match String.lowercase mode_string with
     | "normal" -> `Normal
     | "gz" -> `Gzipped
     | mode -> failwith ("Invalid cache mode: " ^ mode))
@@ -116,6 +143,8 @@ 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
@@ -131,7 +160,11 @@ log_level:\t%d
     (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)
     (String.concat " " (Lazy.force dtd_base_urls))
     (match Lazy.force cache_mode with