added fullscreen menu item

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index d1a39dd9d38c10a65d400159df174a7480109005..5bb01b0f5da52e737233512773397ebe270694ff 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -881,7 +881,7 @@ Copyright (C) 2005,
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image310">
+                               <widget class="GtkImage" id="image318">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
@@ -902,7 +902,7 @@ Copyright (C) 2005,
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image311">
+                               <widget class="GtkImage" id="image319">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
@@ -923,7 +923,7 @@ Copyright (C) 2005,
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image312">
+                               <widget class="GtkImage" id="image320">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</property>
@@ -943,7 +943,7 @@ Copyright (C) 2005,
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image313">
+                               <widget class="GtkImage" id="image321">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
@@ -970,7 +970,7 @@ Copyright (C) 2005,
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image314">
+                               <widget class="GtkImage" id="image322">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
@@ -1023,6 +1023,16 @@ Copyright (C) 2005,
                              <accelerator key="F2" modifiers="0" signal="activate"/>
                            </widget>
                          </child>
+
+                         <child>
+                           <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Fullscreen</property>
+                             <property name="use_underline">True</property>
+                             <property name="active">False</property>
+                             <accelerator key="F11" modifiers="0" signal="activate"/>
+                           </widget>
+                         </child>
                        </widget>
                      </child>
                    </widget>

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 0971cf1bbe3d9625351a98b457158e6e58e84080..d45452a5235176e88a3d27f43cc609d9ebee6b96 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -79,6 +79,9 @@ let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () =
   | None -> ()
   | Some check -> check#set_active (not check#active)
 
+let toggle_callback ~callback ~(check: GMenu.check_menu_item) =
+  ignore (check#connect#toggled (fun _ -> callback check#active))
+  
 let add_key_binding key callback (evbox: GBin.event_box) =
   ignore (evbox#event#connect#key_press (function
     | key' when GdkEvent.Key.keyval key' = key ->

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index 5753293304b52e6470561e4771f785d2c4122151..d18ff281d7f29e7a82cb0188bc5b7da775c83c86 100644 (file)
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -35,6 +35,9 @@ val toggle_window_visibility:
 val toggle_widget_visibility:
   widget:GObj.widget -> check:GMenu.check_menu_item -> unit
 
+val toggle_callback:
+  callback:(bool -> unit) -> check:GMenu.check_menu_item -> unit
+  
 val toggle_win:
   ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit
 

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 *)