F2 hides the tactics buttons bar

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index abab0f7932cf2559a771da7f031222a715f18f49..7256601b6964db394c44812753b85f06282240e9 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -154,6 +154,15 @@ class gui () =
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
       connect_button tbar#autoButton (tac (A.Auto (loc,None)));
+      ignore(self#main#tacticsBarMenuItem#connect#toggled 
+        ~callback:(fun _ -> 
+            if self#main#tacticsBarMenuItem#active then
+                self#main#tacticsButtonsHandlebox#misc#show ()
+            else 
+                self#main#tacticsButtonsHandlebox#misc#hide ()));
+      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;
         (* quit *)
       self#setQuitCallback (fun () -> exit 0);
         (* log *)
@@ -260,7 +269,7 @@ class gui () =
       let height = Gdk.Screen.height () in
       let main_w = width * 90 / 100 in 
       let main_h = height * 80 / 100 in
-      let script_w = main_w / 2 in
+      let script_w = main_w * 6 / 10 in
       self#main#toplevel#resize ~width:main_w ~height:main_h;
       self#main#hpaneScriptSequent#set_position script_w