X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_env.ml;h=1fa159a3cd73c2717a721b73db371e6f9593f62c;hb=23641e7c4b061a2dbc5862d763e8c3602793a94c;hp=be278da6e63eb78fac5e4455bffbbe9d4da9c78c;hpb=b6c8b96f5db84019503c805f7e1d6d5e9aff138e;p=helm.git

diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml
index be278da6e..1fa159a3c 100644
--- a/helm/ocaml/getter/http_getter_env.ml
+++ b/helm/ocaml/getter/http_getter_env.ml
@@ -33,7 +33,7 @@ open Http_getter_types
 let version = Http_getter_const.version
 
 let servers_file    = lazy (
-  Helm_registry.get_opt Helm_registry.get "getter.servers_file")
+  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")
@@ -43,13 +43,13 @@ 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"
+  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.get "rdf_index.txt"
+  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.get "xslt_index.txt"
+  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")
@@ -58,13 +58,15 @@ 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_opt_default Helm_registry.get_string_list
-      ["http://helm.cs.unibo.it/dtd"; "http://mowgli.cs.unibo.it/dtd"]
-      "getter.dtd_base_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_opt_default Helm_registry.get_int 58081 "getter.port")
+  Helm_registry.get_opt_default Helm_registry.int ~default:58081 "getter.port")
 
 let _servers = ref None
 
@@ -79,7 +81,7 @@ let load_servers () =
   match Lazy.force servers_file with
   | None ->
       List.map (fun s -> incr pos; (!pos, s))
-        (Helm_registry.get_string_list "getter.servers")
+        (Helm_registry.get_list Helm_registry.string "getter.servers")
   | Some servers_file ->
       List.rev (Http_getter_misc.fold_file
         (fun line servers ->
@@ -116,7 +118,8 @@ let my_own_url =
 let cache_mode =
   lazy
     (let mode_string =
-      Helm_registry.get_opt_default Helm_registry.get "gz" "getter.cache_mode"
+      Helm_registry.get_opt_default Helm_registry.string ~default:"gz"
+        "getter.cache_mode"
     in
     match String.lowercase mode_string with
     | "normal" -> `Normal