From: Stefano Zacchiroli Date: Wed, 15 Jun 2005 11:32:23 +0000 (+0000) Subject: ported to latest registry interface X-Git-Tag: PRE_STORAGE~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98b94263fd97dc8d580e85ceabae30bf731d58e3;p=helm.git ported to latest registry interface --- diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index c891a0bde..66cc8b0ff 100644 --- 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 58c94ac95..41d62fb38 100644 --- 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 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 diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index afb274f46..dcaee2466 100644 --- 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 67f19879d..bd6e919f9 100644 --- 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 ;