ported to latest registry interface

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c891a0bde63ec069fd9ec1207adde788589aa40a..66cc8b0ffc9ab06aec984c4e205e0ccf720da4ea 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -168,7 +168,9 @@ class gui () =
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:self#main#tacticsBarMenuItem;
       let module Hr = Helm_registry in
-      if not(Hr.get_opt_default Hr.get_bool false "matita.tactics_bar") then 
+      if
+        not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
+      then 
         self#main#tacticsBarMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback 
         ~callback:(function 
@@ -266,8 +268,8 @@ class gui () =
           advance ());
          (* script monospace font stuff *)  
       let font =
-        Helm_registry.get_opt_default Helm_registry.get
-          BuildTimeConf.default_script_font "matita.script_font"
+        Helm_registry.get_opt_default Helm_registry.string
+          ~default:BuildTimeConf.default_script_font "matita.script_font"
       in
 (*       let monospace_tag = 
         source_buffer#create_tag [`FONT_DESC font] 

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 58c94ac957c8dc2ccce93d7546f7bed42ea53ff8..41d62fb380bb966d4dcacef94d99ba7a1eb18125 100644 (file)
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -276,6 +276,7 @@ let resolve_remote uri =
   } in
   let xml_parser = XmlPushParser.create_parser callbacks in
   XmlPushParser.parse xml_parser (`String doc);
+  XmlPushParser.final xml_parser;
   match !res with
   | Unknown -> raise UnexpectedGetterOutput
   | Exception e -> raise e
@@ -650,12 +651,14 @@ let sync_dump_file () =
   
 let init () =
   Http_getter_logger.set_log_level
-    (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+    (Helm_registry.get_opt_default Helm_registry.int ~default:1
+      "getter.log_level");
   Http_getter_logger.set_log_file
-    (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+    (Helm_registry.get_opt Helm_registry.string "getter.log_file");
   Http_getter_env.reload ();
   let is_prefetch_set = 
-    Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch"
+    Helm_registry.get_opt_default Helm_registry.bool ~default:false
+      "getter.prefetch"
   in
   if is_prefetch_set then
     (* ignore (Thread.create sync_with_map ()) *)

diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml
index be278da6e63eb78fac5e4455bffbbe9d4da9c78c..1fa159a3cd73c2717a721b73db371e6f9593f62c 100644 (file)
--- 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

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index afb274f460e07f008d746d2fee0be5ac3f8182c0..dcaee2466dc13a0c4a61c22d0de3ff1c5ee45d27 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -467,7 +467,7 @@ let callback dbd (req: Http_types.request) outchan =
 
 let restore_environment () =
   match
-    Helm_registry.get_opt Helm_registry.get "search_engine.environment_dump"
+    Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump"
   with
   | None -> ()
   | Some fname ->

diff --git a/helm/uwobo/uwobo_profiles.ml b/helm/uwobo/uwobo_profiles.ml
index 67f19879d8ff13058a3a188ee94f59eaf3af144e..bd6e919f94ebcb40531c8551fb8e89f0ddcf07de 100644 (file)
--- a/helm/uwobo/uwobo_profiles.ml
+++ b/helm/uwobo/uwobo_profiles.ml
@@ -94,7 +94,8 @@ let to_list_rel ~prefix () =
 let check_permission pid password for_what =
   match password, Helm_registry.get_bool (permission_key for_what pid) with
       _, true -> ()
-    | Some pwd, false when Some pwd = Helm_registry.get_opt Helm_registry.get (password_key pid) -> ()
+    | Some pwd, false
+      when Some pwd = Helm_registry.get_opt Helm_registry.string (password_key pid) -> ()
     | _ -> raise (Access_denied (string_of_permission for_what, pid))
 
 let create ?id ?clone ?clone_password ?(read_perm=true) ?(write_perm=true) ?(admin_perm=true) ?password () =
@@ -115,7 +116,7 @@ let create ?id ?clone ?clone_password ?(read_perm=true) ?(write_perm=true) ?(adm
     Helm_registry.set_bool (read_permission_key pid) read_perm ;
     Helm_registry.set_bool (write_permission_key pid) write_perm ;
     Helm_registry.set_bool (admin_permission_key pid) admin_perm ;
-    Helm_registry.set_opt Helm_registry.set_string (password_key pid) password ;
+    Helm_registry.set_opt Helm_registry.of_string (password_key pid) password ;
     pid
 
 let remove pid ?password () =
@@ -138,7 +139,7 @@ let get_param pid ?password ~key () =
 
 let set_password pid ?old_password new_password =
   check_permission pid old_password `Admin ;
-  Helm_registry.set_opt Helm_registry.set (password_key pid) new_password
+  Helm_registry.set_opt Helm_registry.of_string (password_key pid) new_password
 
 let set_permission pid ?password for_what value =
   check_permission pid password `Admin ;