From 5602ae08829342b7c2526053a5cb27cffe8a3d52 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 14 Jun 2005 07:57:51 +0000
Subject: [PATCH] added fullscreen menu item

---
 helm/matita/matita.glade      | 20 +++++++++++++++-----
 helm/matita/matitaGtkMisc.ml  |  3 +++
 helm/matita/matitaGtkMisc.mli |  3 +++
 helm/matita/matitaGui.ml      |  6 ++++++
 4 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index d1a39dd9d..5bb01b0f5 100644
--- 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 0971cf1bb..d45452a52 100644
--- 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 575329330..d18ff281d 100644
--- 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 b6b3f5ea2..c891a0bde 100644
--- 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 *)
-- 
2.39.2