Change Sort.merge (deprecated) with List.merge

[helm.git] / matita / matita / matita.glade

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index 6d4b5967209bb58831d39c8f8e8b5895f6e36a26..85c9f280940226c4e8335b5cadabbcbbf278156a 100644 (file)
--- 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>
@@ -212,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>
@@ -693,6 +701,15 @@
                                 <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">gtk-quit</property>
@@ -1681,23 +1698,11 @@
                                 <property name="can_focus">True</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>