From: Enrico Tassi Date: Mon, 13 Jun 2005 14:45:57 +0000 (+0000) Subject: F2 hides the tactics buttons bar X-Git-Tag: PRE_STORAGE~46 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98af6b692e80b3ce45886b89100812047d67c3bd;p=helm.git F2 hides the tactics buttons bar --- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 9444e6a93..bea43910b 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -881,7 +881,7 @@ Copyright (C) 2005, True - + True gtk-new 1 @@ -902,7 +902,7 @@ Copyright (C) 2005, - + True gtk-open 1 @@ -923,7 +923,7 @@ Copyright (C) 2005, - + True gtk-save 1 @@ -943,7 +943,7 @@ Copyright (C) 2005, True - + True gtk-save-as 1 @@ -970,7 +970,7 @@ Copyright (C) 2005, - + True gtk-quit 1 @@ -1012,6 +1012,17 @@ Copyright (C) 2005, + + + + True + Show/Hide the tactics buttons bar + View Tactics Bar + True + True + + + @@ -1073,937 +1084,931 @@ Copyright (C) 2005, 0 - - 2 + True - GTK_SHADOW_OUT - GTK_POS_TOP - GTK_POS_LEFT + True - + True - 17 - 2 False - 4 - 0 + 0 - - 50 + True - Apply - True - apply - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 0 - 1 - fill - - - + GTK_SHADOW_OUT + GTK_POS_TOP + GTK_POS_TOP - - - 55 - True - Intros - True - intro - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 0 - 1 - fill - - - + + + True + 17 + 2 + False + 4 + 0 - - - 55 - True - Exact - True - exact - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 2 - 3 - fill - - - + + + True + Apply + True + apply + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 0 + 1 + fill + + + - - - 55 - True - Elim - True - elim - True - GTK_RELIEF_HALF - True - - - 0 - 1 - 4 - 5 - fill - - - + + + True + Intros + True + intro + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 0 + 1 + fill + + + - - - 55 - True - Reflexivity - True - refl - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 8 - 9 - fill - - - + + + True + Exact + True + exact + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 2 + 3 + fill + + + - - - 50 - True - Symmetry - True - sym - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 8 - 9 - fill - - - + + + True + Elim + True + elim + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 4 + 5 + fill + + + - - - 55 - True - Transitivity - True - trans - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 9 - 10 - fill - - - + + + True + Reflexivity + True + refl + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 8 + 9 + fill + + + - - - 55 - True - Simplify - True - simpl - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 11 - 12 - fill - - - + + + True + Symmetry + True + sym + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 8 + 9 + fill + + + - - - 50 - True - Reduce - True - red - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 11 - 12 - fill - - - + + + True + Transitivity + True + trans + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 9 + 10 + fill + + + - - - 55 - True - Whd - True - whd - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 12 - 13 - fill - - - + + + True + Simplify + True + simpl + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 11 + 12 + fill + + + - - - 55 - True - Assumption - True - assum - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 14 - 15 - fill - - - + + + True + Reduce + True + red + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 11 + 12 + fill + + + - - - 50 - True - Auto - True - auto - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 14 - 15 - fill - - - + + + True + Whd + True + whd + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 12 + 13 + fill + + + - - - 55 - True - Cut - True - cut - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 16 - 17 - fill - - - + + + True + Assumption + True + assum + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 14 + 15 + fill + + + - - - 50 - True - Replace - True - repl - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 16 - 17 - fill - - - + + + True + Auto + True + auto + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 14 + 15 + fill + + + - - - 55 - True - ElimType - True - elimTy - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 4 - 5 - fill - - - + + + True + Cut + True + cut + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 16 + 17 + fill + + + - - - True - False - 0 + + + True + Replace + True + repl + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 16 + 17 + fill + + + - - - 25 - True - Right - True - R - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - + + + True + ElimType + True + elimTy + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 4 + 5 + fill + + + - - - 25 - True - Exists - True - ∃ - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - 1 - 2 - 6 - 7 - fill - fill - - + + + True + True + 0 - - - True - False - 0 + + + True + Right + True + R + True + GTK_RELIEF_NORMAL + True + + + 0 + True + True + + - - - 25 - True - Split - True - ∧ - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - + + + True + Exists + True + ∃ + True + GTK_RELIEF_NORMAL + True + + + 0 + True + True + + + + + 1 + 2 + 6 + 7 + fill + fill + + - - - 25 - True - Left - True - L - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - 0 - 1 - 6 - 7 - fill - fill - - + + + True + True + 0 - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + Split + True + ∧ + True + GTK_RELIEF_NORMAL + True + + + 0 + True + True + + - - - - - - 0 - 1 - 1 - 2 - fill - - + + + True + Left + True + L + True + GTK_RELIEF_NORMAL + True + + + 0 + True + True + + + + + 0 + 1 + 6 + 7 + fill + fill + + + + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + + + + + 0 + 1 + 1 + 2 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - - - - - 0 - 1 - 3 - 4 - fill - - + + + + + + 0 + 1 + 3 + 4 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - - - - - 0 - 1 - 5 - 6 - fill - - + + + + + + 0 + 1 + 5 + 6 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - - - - - 0 - 1 - 7 - 8 - fill - - + + + + + + 0 + 1 + 7 + 8 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - - - - - 0 - 1 - 10 - 11 - fill - - + + + + + + 0 + 1 + 10 + 11 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - - - - - 0 - 1 - 13 - 14 - fill - - + + + + + + 0 + 1 + 13 + 14 + fill + + - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - + + + + + + 0 + 1 + 15 + 16 + fill + + + - 0 - 1 - 15 - 16 - fill + 0 + False + True - - - - - 0 - False - True - - - - - - True - True - - - - 400 - True - False - 0 - + + 400 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + False + 0 - + True - True - True - False + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - restart (Home) - True - GTK_RELIEF_NONE - True - + True + True + False - + True - gtk-goto-top - 4 - 0.5 - 0.5 - 0 - 0 + restart (Home) + True + GTK_RELIEF_NONE + True + + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - go back 1 phrase (Page Up) - True - GTK_RELIEF_NONE - True - + True + True + False - + True - gtk-go-up - 4 - 0.5 - 0.5 - 0 - 0 + go back 1 phrase (Page Up) + True + GTK_RELIEF_NONE + True + + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - execute until point - True - GTK_RELIEF_NONE - True + True + True + False - + True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 + execute until point + True + GTK_RELIEF_NONE + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - go forward 1 phrase (Page Down) - True - GTK_RELIEF_NONE - True - + True + True + False - + True - gtk-go-down - 4 - 0.5 - 0.5 - 0 - 0 + go forward 1 phrase (Page Down) + True + GTK_RELIEF_NONE + True + + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - execute all (End) - True - GTK_RELIEF_NONE - True - + True + True + False - + True - gtk-goto-bottom - 4 - 0.5 - 0.5 - 0 - 0 + execute all (End) + True + GTK_RELIEF_NONE + True + + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + + 0 False - False + False - - - 0 - False - False - - - - - - True - True - True - True - GTK_POS_BOTTOM - False - False - + True True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT + True + True + GTK_POS_BOTTOM + False + False - + True True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + 2 + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 2 + 0 + 0 + + + + + False + True + - - - False - True - - - - - - True - script - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + - + True True - False - False - False - True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + False + True + - - - False - True - - - - - True - outline - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + + + True + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + - tab + 0 + True + True @@ -2093,7 +2098,7 @@ Copyright (C) 2005, - False + True True diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index abab0f793..7256601b6 100644 --- 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