X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.glade;h=85c9f280940226c4e8335b5cadabbcbbf278156a;hb=a4ba77d9df157e443e6fb39dc7376996faea9973;hp=46023a02ef1d456b7686795a6492fcdf7ce7f8ee;hpb=7be382111340d6240b45e95126c7844134272b41;p=helm.git

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index 46023a02e..85c9f2809 100644
--- a/matita/matita/matita.glade
+++ b/matita/matita/matita.glade
@@ -1,6 +1,6 @@
 <?xml version="1.0"?>
 <glade-interface>
-  <!-- interface-requires gtk+ 2.6 -->
+  <!-- interface-requires gtk+ 2.16 -->
   <!-- interface-naming-policy toplevel-contextual -->
   <widget class="GtkWindow" id="BrowserWin">
     <property name="width_request">500</property>
@@ -80,24 +80,6 @@
                     </child>
                   </widget>
                 </child>
-                <child>
-                  <widget class="GtkMenuItem" id="BrowserViewMenu">
-                    <property name="visible">True</property>
-                    <property name="label" translatable="yes">_View</property>
-                    <property name="use_underline">True</property>
-                    <child>
-                      <widget class="GtkMenu" id="BrowserViewMenu_menu">
-                        <child>
-                          <widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
-                            <property name="visible">True</property>
-                            <property name="label" translatable="yes">HBugs Tutors</property>
-                            <property name="use_underline">True</property>
-                          </widget>
-                        </child>
-                      </widget>
-                    </child>
-                  </widget>
-                </child>
               </widget>
               <packing>
                 <property name="expand">False</property>
@@ -230,7 +212,15 @@
                       <widget class="GtkHBox" id="UriHBox">
                         <property name="visible">True</property>
                         <child>
-                          <placeholder/>
+                          <widget class="GtkEntry" id="browserUri">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="has_focus">True</property>
+                            <property name="invisible_char">&#x25CF;</property>
+                          </widget>
+                          <packing>
+                            <property name="position">0</property>
+                          </packing>
                         </child>
                       </widget>
                       <packing>
@@ -290,9 +280,9 @@
                   </packing>
                 </child>
                 <child>
-                  <widget class="GtkLabel" id="listLabel">
+                  <widget class="GtkLabel" id="WhelpResult">
                     <property name="visible">True</property>
-                    <property name="label" translatable="yes">WhelpResults</property>
+                    <property name="label" translatable="yes">WhelpResult</property>
                   </widget>
                   <packing>
                     <property name="position">1</property>
@@ -359,131 +349,6 @@
                     <property name="type">tab</property>
                   </packing>
                 </child>
-                <child>
-                  <widget class="GtkVBox" id="vbox16">
-                    <property name="visible">True</property>
-                    <property name="orientation">vertical</property>
-                    <child>
-                      <widget class="GtkScrolledWindow" id="scrolledwindow13">
-                        <property name="visible">True</property>
-                        <property name="can_focus">True</property>
-                        <child>
-                          <widget class="GtkTreeView" id="HBugsTutorsList">
-                            <property name="visible">True</property>
-                            <property name="can_focus">True</property>
-                          </widget>
-                        </child>
-                      </widget>
-                      <packing>
-                        <property name="position">0</property>
-                      </packing>
-                    </child>
-                    <child>
-                      <widget class="GtkToolbar" id="toolbar3">
-                        <property name="visible">True</property>
-                        <property name="toolbar_style">both</property>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem47">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsRefreshButton">
-                                <property name="label">gtk-refresh</property>
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="receives_default">False</property>
-                                <property name="use_stock">True</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem48">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsUnsubscribeButton">
-                                <property name="label">gtk-remove</property>
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="receives_default">False</property>
-                                <property name="use_stock">True</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem49">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsSubscribeButton">
-                                <property name="label">gtk-add</property>
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="receives_default">False</property>
-                                <property name="use_stock">True</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                          </packing>
-                        </child>
-                      </widget>
-                      <packing>
-                        <property name="expand">False</property>
-                        <property name="fill">False</property>
-                        <property name="position">1</property>
-                      </packing>
-                    </child>
-                  </widget>
-                  <packing>
-                    <property name="position">4</property>
-                  </packing>
-                </child>
-                <child>
-                  <widget class="GtkLabel" id="label29">
-                    <property name="visible">True</property>
-                    <property name="label" translatable="yes">HBugs</property>
-                  </widget>
-                  <packing>
-                    <property name="position">4</property>
-                    <property name="tab_fill">False</property>
-                    <property name="type">tab</property>
-                  </packing>
-                </child>
-                <child>
-                  <widget class="GtkScrolledWindow" id="textScrolledWin">
-                    <property name="visible">True</property>
-                    <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">automatic</property>
-                    <property name="vscrollbar_policy">automatic</property>
-                    <child>
-                      <widget class="GtkTreeView" id="universesTreeview">
-                        <property name="visible">True</property>
-                        <property name="can_focus">True</property>
-                      </widget>
-                    </child>
-                  </widget>
-                  <packing>
-                    <property name="position">5</property>
-                  </packing>
-                </child>
-                <child>
-                  <widget class="GtkLabel" id="universes">
-                    <property name="visible">True</property>
-                    <property name="label" translatable="yes">Universes</property>
-                  </widget>
-                  <packing>
-                    <property name="position">5</property>
-                    <property name="tab_fill">False</property>
-                    <property name="type">tab</property>
-                  </packing>
-                </child>
                 <child>
                   <widget class="GtkVBox" id="vbox20">
                     <property name="visible">True</property>
@@ -590,16 +455,16 @@
                     </child>
                   </widget>
                   <packing>
-                    <property name="position">6</property>
+                    <property name="position">4</property>
                   </packing>
                 </child>
                 <child>
-                  <widget class="GtkLabel" id="label1">
+                  <widget class="GtkLabel" id="SearchText">
                     <property name="visible">True</property>
                     <property name="label" translatable="yes">SearchText</property>
                   </widget>
                   <packing>
-                    <property name="position">6</property>
+                    <property name="position">4</property>
                     <property name="tab_fill">False</property>
                     <property name="type">tab</property>
                   </packing>
@@ -797,7 +662,7 @@
                           <widget class="GtkMenu" id="fileMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="newMenuItem">
-                                <property name="label">_New</property>
+                                <property name="label">gtk-new</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -806,7 +671,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="openMenuItem">
-                                <property name="label">_Open...</property>
+                                <property name="label">gtk-open</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -815,7 +680,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="saveMenuItem">
-                                <property name="label">_Save</property>
+                                <property name="label">gtk-save</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -824,7 +689,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="saveAsMenuItem">
-                                <property name="label">Save _as ...</property>
+                                <property name="label">gtk-save-as</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -836,9 +701,18 @@
                                 <property name="visible">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkImageMenuItem" id="closeMenuItem">
+                                <property name="label">gtk-close</property>
+                                <property name="visible">True</property>
+                                <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
+                                <accelerator key="w" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="quitMenuItem">
-                                <property name="label">_Quit</property>
+                                <property name="label">gtk-quit</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -858,7 +732,7 @@
                           <widget class="GtkMenu" id="editMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="undoMenuItem">
-                                <property name="label">_Undo</property>
+                                <property name="label">gtk-undo</property>
                                 <property name="visible">True</property>
                                 <property name="sensitive">False</property>
                                 <property name="use_underline">True</property>
@@ -868,7 +742,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="redoMenuItem">
-                                <property name="label">_Redo</property>
+                                <property name="label">gtk-redo</property>
                                 <property name="visible">True</property>
                                 <property name="sensitive">False</property>
                                 <property name="use_underline">True</property>
@@ -883,7 +757,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="cutMenuItem">
-                                <property name="label">Cu_t</property>
+                                <property name="label">gtk-cut</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -892,7 +766,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="copyMenuItem">
-                                <property name="label">_Copy</property>
+                                <property name="label">gtk-copy</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -901,7 +775,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="pasteMenuItem">
-                                <property name="label">_Paste</property>
+                                <property name="label">gtk-paste</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -933,7 +807,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
-                                <property name="label">_Delete</property>
+                                <property name="label">gtk-delete</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -958,7 +832,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="findReplMenuItem">
-                                <property name="label">_Find &amp; replace ...</property>
+                                <property name="label">gtk-find-and-replace</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -997,18 +871,20 @@
                         <child>
                           <widget class="GtkMenu" id="scriptMenu_menu">
                             <child>
-                              <widget class="GtkMenuItem" id="scriptAdvanceMenuItem">
+                              <widget class="GtkImageMenuItem" id="scriptAdvanceMenuItem">
+                                <property name="label">gtk-go-down</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Execute 1 phrase</property>
                                 <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
                                 <accelerator key="Page_Down" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkMenuItem" id="scriptRetractMenuItem">
+                              <widget class="GtkImageMenuItem" id="scriptRetractMenuItem">
+                                <property name="label">gtk-go-up</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Retract 1 phrase</property>
                                 <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
                                 <accelerator key="Page_Up" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
@@ -1018,18 +894,20 @@
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkMenuItem" id="scriptBottomMenuItem">
+                              <widget class="GtkImageMenuItem" id="scriptBottomMenuItem">
+                                <property name="label">gtk-goto-bottom</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Execute all</property>
                                 <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
                                 <accelerator key="End" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkMenuItem" id="scriptTopMenuItem">
+                              <widget class="GtkImageMenuItem" id="scriptTopMenuItem">
+                                <property name="label">gtk-goto-top</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Restart</property>
                                 <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
                                 <accelerator key="Home" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
@@ -1039,10 +917,11 @@
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkMenuItem" id="scriptJumpMenuItem">
+                              <widget class="GtkImageMenuItem" id="scriptJumpMenuItem">
+                                <property name="label">gtk-jump-to</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Execute until cursor</property>
                                 <property name="use_underline">True</property>
+                                <property name="use_stock">True</property>
                                 <accelerator key="period" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
@@ -1094,7 +973,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
-                                <property name="label">Zoom _in</property>
+                                <property name="label">gtk-zoom-in</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -1103,7 +982,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
-                                <property name="label">Zoom _out</property>
+                                <property name="label">gtk-zoom-out</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -1112,7 +991,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
-                                <property name="label">_Normal size</property>
+                                <property name="label">gtk-zoom-100</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -1170,12 +1049,11 @@
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkImageMenuItem" id="showUnicodeTable">
-                                <property name="label">TeX/UTF-8 table</property>
+                              <widget class="GtkMenuItem" id="showUnicodeTable">
                                 <property name="visible">True</property>
                                 <property name="tooltip" translatable="yes">Show the conversion table from TeX like sequences to UTF-8</property>
+                                <property name="label" translatable="yes">TeX/UTF-8 table</property>
                                 <property name="use_underline">True</property>
-                                <property name="use_stock">True</property>
                               </widget>
                             </child>
                           </widget>
@@ -1207,7 +1085,7 @@
                           <widget class="GtkMenu" id="helpMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="contentsMenuItem">
-                                <property name="label">_Contents</property>
+                                <property name="label">gtk-help</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -1216,7 +1094,7 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
-                                <property name="label">_About</property>
+                                <property name="label">gtk-about</property>
                                 <property name="visible">True</property>
                                 <property name="use_underline">True</property>
                                 <property name="use_stock">True</property>
@@ -1818,58 +1696,22 @@
                               <widget class="GtkNotebook" id="scriptNotebook">
                                 <property name="visible">True</property>
                                 <property name="can_focus">True</property>
-                                <property name="tab_pos">bottom</property>
+                                <property name="scrollable">True</property>
                                 <child>
-                                  <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
-                                    <property name="visible">True</property>
-                                    <property name="can_focus">True</property>
-                                    <property name="hscrollbar_policy">automatic</property>
-                                    <property name="vscrollbar_policy">automatic</property>
-                                    <child>
-                                      <placeholder/>
-                                    </child>
-                                  </widget>
+                                  <placeholder/>
                                 </child>
                                 <child>
-                                  <widget class="GtkLabel" id="scriptLabel">
-                                    <property name="visible">True</property>
-                                    <property name="label" translatable="yes">script</property>
-                                  </widget>
+                                  <placeholder/>
                                   <packing>
-                                    <property name="tab_fill">False</property>
                                     <property name="type">tab</property>
                                   </packing>
                                 </child>
                                 <child>
-                                  <widget class="GtkScrolledWindow" id="scrolledwindow8">
-                                    <property name="visible">True</property>
-                                    <property name="can_focus">True</property>
-                                    <property name="hscrollbar_policy">automatic</property>
-                                    <property name="vscrollbar_policy">automatic</property>
-                                    <child>
-                                      <widget class="GtkViewport" id="viewport1">
-                                        <property name="visible">True</property>
-                                        <child>
-                                          <widget class="GtkLabel" id="label25">
-                                            <property name="visible">True</property>
-                                            <property name="label" translatable="yes">Not implemented.</property>
-                                          </widget>
-                                        </child>
-                                      </widget>
-                                    </child>
-                                  </widget>
-                                  <packing>
-                                    <property name="position">1</property>
-                                  </packing>
+                                  <placeholder/>
                                 </child>
                                 <child>
-                                  <widget class="GtkLabel" id="label13">
-                                    <property name="visible">True</property>
-                                    <property name="label" translatable="yes">outline</property>
-                                  </widget>
+                                  <placeholder/>
                                   <packing>
-                                    <property name="position">1</property>
-                                    <property name="tab_fill">False</property>
                                     <property name="type">tab</property>
                                   </packing>
                                 </child>
@@ -1900,6 +1742,7 @@
                           <widget class="GtkNotebook" id="sequentsNotebook">
                             <property name="visible">True</property>
                             <property name="can_focus">True</property>
+                            <property name="scrollable">True</property>
                           </widget>
                           <packing>
                             <property name="resize">False</property>