fix

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index b6b3f5ea2fd6efa7bdda78ed3fd4f63850ddbd17..66cc8b0ffc9ab06aec984c4e205e0ccf720da4ea 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -168,8 +168,16 @@ 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 
+          | true -> self#main#toplevel#fullscreen () 
+          | false -> self#main#toplevel#unfullscreen ())
+        ~check:self#main#fullscreenMenuItem;
+      self#main#fullscreenMenuItem#set_active false;
         (* quit *)
       self#setQuitCallback (fun () -> exit 0);
         (* log *)
@@ -260,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]