findReplace ported from GtkTable to GtkGrid

diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui
index 47987930e881a49868e95b4d60c7d80a44174645..f1f674ec132d85ada5c58746aa32a4f03632a18f 100644 (file)
--- a/matita/matita/matita.ui
+++ b/matita/matita/matita.ui
@@ -139,7 +139,6 @@
           <object class="GtkSeparator" id="hseparator3">
             <property name="visible">True</property>
             <property name="can_focus">False</property>
-            <property name="orientation">horizontal</property>
           </object>
           <packing>
             <property name="expand">False</property>
@@ -172,7 +171,6 @@
                 <property name="border_width">4</property>
                 <property name="spacing">4</property>
                 <property name="layout_style">end</property>
-                <property name="orientation">horizontal</property>
                 <child>
                   <object class="GtkButton" id="buttonPAUSE">
                     <property name="label">gtk-media-pause</property>
@@ -1081,12 +1079,10 @@
     <property name="window_position">mouse</property>
     <property name="type_hint">dialog</property>
     <child>
-      <object class="GtkTable" id="table1">
+      <object class="GtkGrid" id="table1">
         <property name="visible">True</property>
         <property name="can_focus">False</property>
-        <property name="n_rows">3</property>
-        <property name="n_columns">2</property>
-        <property name="row_spacing">5</property>
+        <property name="row_spacing">9</property>
         <child>
           <object class="GtkLabel" id="label17">
             <property name="visible">True</property>
@@ -1095,8 +1091,8 @@
             <property name="xalign">0</property>
           </object>
           <packing>
-            <property name="x_options"/>
-            <property name="y_options"/>
+            <property name="left_attach">0</property>
+            <property name="top_attach">0</property>
           </packing>
         </child>
         <child>
@@ -1107,24 +1103,20 @@
             <property name="xalign">0</property>
           </object>
           <packing>
+            <property name="left_attach">0</property>
             <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="x_options"/>
-            <property name="y_options"/>
           </packing>
         </child>
         <child>
           <object class="GtkEntry" id="findEntry">
             <property name="visible">True</property>
             <property name="can_focus">True</property>
-            <property name="has_focus">True</property>
             <property name="can_default">True</property>
             <property name="has_default">True</property>
           </object>
           <packing>
             <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="y_options"/>
+            <property name="top_attach">0</property>
           </packing>
         </child>
         <child>
@@ -1134,10 +1126,7 @@
           </object>
           <packing>
             <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
             <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="y_options"/>
           </packing>
         </child>
         <child>
@@ -1145,18 +1134,7 @@
             <property name="visible">True</property>
             <property name="can_focus">False</property>
             <property name="spacing">5</property>
-            <child>
-              <object class="GtkBox" id="vbox9">
-                <property name="visible">True</property>
-                <property name="can_focus">False</property>
-                <property name="orientation">vertical</property>
-              </object>
-              <packing>
-                <property name="expand">True</property>
-                <property name="fill">True</property>
-                <property name="position">0</property>
-              </packing>
-            </child>
+            <property name="homogeneous">True</property>
             <child>
               <object class="GtkButton" id="findButton">
                 <property name="label">gtk-find</property>
@@ -1239,10 +1217,9 @@
             </child>
           </object>
           <packing>
-            <property name="right_attach">2</property>
+            <property name="left_attach">0</property>
             <property name="top_attach">2</property>
-            <property name="bottom_attach">3</property>
-            <property name="y_padding">5</property>
+            <property name="width">2</property>
           </packing>
         </child>
       </object>
@@ -1763,7 +1740,6 @@
                   <object class="GtkPaned" id="hpaneScriptSequent">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="orientation">horizontal</property>
                     <child>
                       <object class="GtkBox" id="hbox18">
                         <property name="visible">True</property>
@@ -2213,6 +2189,11 @@
                                   </packing>
                                 </child>
                               </object>
+                              <packing>
+                                <property name="expand">False</property>
+                                <property name="fill">True</property>
+                                <property name="position">0</property>
+                              </packing>
                             </child>
                           </object>
                           <packing>
@@ -2449,8 +2430,8 @@
                         <property name="height_request">500</property>
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
-                        <property name="position">380</property>
                         <property name="orientation">vertical</property>
+                        <property name="position">380</property>
                         <child>
                           <object class="GtkNotebook" id="sequentsNotebook">
                             <property name="visible">True</property>