From: Claudio Sacerdoti Coen Date: Wed, 20 Jul 2005 14:11:53 +0000 (+0000) Subject: Several interface improvements here and there. X-Git-Tag: V_0_7_2~145 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bbfb0dbb2d5acd97014b8d4f0285c5a53d7d1b0;p=helm.git Several interface improvements here and there. The interface is now closer to the Gnome Interface Guidelines. --- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 2fb05862d..2e4a84f55 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 @@ -964,7 +964,7 @@ Copyright (C) 2005, - + True gtk-execute 1 @@ -991,7 +991,7 @@ Copyright (C) 2005, - + True gtk-quit 1 @@ -1021,12 +1021,12 @@ Copyright (C) 2005, True False - Undo + _Undo True - + True gtk-undo 1 @@ -1043,12 +1043,12 @@ Copyright (C) 2005, True False - Redo + _Redo True - + True gtk-redo 1 @@ -1070,12 +1070,12 @@ Copyright (C) 2005, True - Cut + Cu_t True - + True gtk-cut 1 @@ -1091,12 +1091,12 @@ Copyright (C) 2005, True - Copy + _Copy True - + True gtk-copy 1 @@ -1112,12 +1112,12 @@ Copyright (C) 2005, True - Paste + _Paste True - + True gtk-paste 1 @@ -1133,11 +1133,11 @@ Copyright (C) 2005, True - Delete + _Delete True - + True gtk-delete 1 @@ -1159,12 +1159,12 @@ Copyright (C) 2005, True - Find & Replace + _Find & Replace True - + True gtk-find-and-replace 1 @@ -1194,7 +1194,7 @@ Copyright (C) 2005, True Show/Hide the tactics buttons bar - View Tactics Bar + View _Tactics Bar True True @@ -1204,7 +1204,7 @@ Copyright (C) 2005, True - New Cic Browser + New Cic _Browser True @@ -1219,7 +1219,7 @@ Copyright (C) 2005, True - Fullscreen + _Fullscreen True False @@ -1233,31 +1233,67 @@ Copyright (C) 2005, - + True - Increase Font Size + Zoom _In True + + + + True + gtk-zoom-in + 1 + 0.5 + 0.5 + 0 + 0 + + - + True - Decrease Font Size + Zoom _Out True + + + + True + gtk-zoom-out + 1 + 0.5 + 0.5 + 0 + 0 + + - + True - Normal Font Size + _Normal Size True + + + + True + gtk-zoom-100 + 1 + 0.5 + 0.5 + 0 + 0 + + @@ -1268,14 +1304,14 @@ Copyright (C) 2005, True - Debug + _Debug True - + True @@ -1294,10 +1330,22 @@ Copyright (C) 2005, - + True - About... + _About True + + + + True + gtk-about + 1 + 0.5 + 0.5 + 0 + 0 + +