ported to latest registry interface

[helm.git] / helm / matita / matitaGui.ml

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]