X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaGui.ml;h=66cc8b0ffc9ab06aec984c4e205e0ccf720da4ea;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=b6b3f5ea2fd6efa7bdda78ed3fd4f63850ddbd17;hpb=25d3d1c2613fd2b4e6a323289ca94fb7b75ebe5d;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index b6b3f5ea2..66cc8b0ff 100644
--- 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]