]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/http_getter_env.ml
ported to latest registry interface
[helm.git] / helm / ocaml / getter / http_getter_env.ml
index be278da6e63eb78fac5e4455bffbbe9d4da9c78c..1fa159a3cd73c2717a721b73db371e6f9593f62c 100644 (file)
@@ -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