added fullscreen menu item

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index b6b3f5ea2fd6efa7bdda78ed3fd4f63850ddbd17..c891a0bde63ec069fd9ec1207adde788589aa40a 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -170,6 +170,12 @@ class gui () =
       let module Hr = Helm_registry in
       if not(Hr.get_opt_default Hr.get_bool 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 *)