X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.glade;h=85c9f280940226c4e8335b5cadabbcbbf278156a;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=3b87423d0e2f3a18f4a21ccb0423eee1a8f0186f;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index 3b87423d0..85c9f2809 100644
--- a/matita/matita/matita.glade
+++ b/matita/matita/matita.glade
@@ -1,13 +1,13 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<!DOCTYPE glade-interface SYSTEM "glade-2.0.dtd">
-<!--*- mode: xml -*-->
+<?xml version="1.0"?>
 <glade-interface>
+  <!-- interface-requires gtk+ 2.16 -->
+  <!-- interface-naming-policy toplevel-contextual -->
   <widget class="GtkWindow" id="BrowserWin">
     <property name="width_request">500</property>
     <property name="height_request">480</property>
     <property name="visible">True</property>
     <property name="title" translatable="yes">Cic browser</property>
-    <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
+    <property name="window_position">center-on-parent</property>
     <property name="default_width">500</property>
     <property name="default_height">480</property>
     <property name="destroy_with_parent">True</property>
@@ -17,6 +17,7 @@
         <child>
           <widget class="GtkVBox" id="BrowserVBox">
             <property name="visible">True</property>
+            <property name="orientation">vertical</property>
             <child>
               <widget class="GtkMenuBar" id="menubar2">
                 <property name="visible">True</property>
@@ -29,8 +30,8 @@
                       <widget class="GtkMenu" id="BrowserFileMenu_menu">
                         <child>
                           <widget class="GtkImageMenuItem" id="BrowserNewMenuItem">
-                            <property name="visible">True</property>
                             <property name="label">gtk-new</property>
+                            <property name="visible">True</property>
                             <property name="use_underline">True</property>
                             <property name="use_stock">True</property>
                           </widget>
@@ -40,7 +41,7 @@
                             <property name="visible">True</property>
                             <property name="label" translatable="yes">Open _Location ...</property>
                             <property name="use_underline">True</property>
-                            <accelerator key="L" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+                            <accelerator key="L" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                           </widget>
                         </child>
                         <child>
@@ -50,8 +51,8 @@
                         </child>
                         <child>
                           <widget class="GtkImageMenuItem" id="BrowserCloseMenuItem">
-                            <property name="visible">True</property>
                             <property name="label">gtk-close</property>
+                            <property name="visible">True</property>
                             <property name="use_underline">True</property>
                             <property name="use_stock">True</property>
                           </widget>
@@ -69,28 +70,10 @@
                       <widget class="GtkMenu" id="BrowserEditMenu_menu">
                         <child>
                           <widget class="GtkImageMenuItem" id="BrowserCopyMenuItem">
-                            <property name="visible">True</property>
                             <property name="label">gtk-copy</property>
-                            <property name="use_underline">True</property>
-                            <property name="use_stock">True</property>
-                          </widget>
-                        </child>
-                      </widget>
-                    </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>
+                            <property name="use_stock">True</property>
                           </widget>
                         </child>
                       </widget>
@@ -101,6 +84,7 @@
               <packing>
                 <property name="expand">False</property>
                 <property name="fill">False</property>
+                <property name="position">0</property>
               </packing>
             </child>
             <child>
@@ -108,7 +92,7 @@
                 <property name="visible">True</property>
                 <property name="label_xalign">0</property>
                 <property name="label_yalign">0</property>
-                <property name="shadow_type">GTK_SHADOW_NONE</property>
+                <property name="shadow_type">none</property>
                 <child>
                   <widget class="GtkHBox" id="BrowserHBox">
                     <property name="visible">True</property>
@@ -116,8 +100,8 @@
                       <widget class="GtkButton" id="BrowserNewButton">
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
-                        <property name="relief">GTK_RELIEF_NONE</property>
-                        <property name="response_id">0</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
                         <child>
                           <widget class="GtkImage" id="image303">
                             <property name="visible">True</property>
@@ -128,14 +112,15 @@
                       <packing>
                         <property name="expand">False</property>
                         <property name="fill">False</property>
+                        <property name="position">0</property>
                       </packing>
                     </child>
                     <child>
                       <widget class="GtkButton" id="BrowserBackButton">
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
-                        <property name="relief">GTK_RELIEF_NONE</property>
-                        <property name="response_id">0</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
                         <child>
                           <widget class="GtkImage" id="image304">
                             <property name="visible">True</property>
@@ -153,8 +138,8 @@
                       <widget class="GtkButton" id="BrowserForwardButton">
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
-                        <property name="relief">GTK_RELIEF_NONE</property>
-                        <property name="response_id">0</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
                         <child>
                           <widget class="GtkImage" id="image305">
                             <property name="visible">True</property>
@@ -173,9 +158,9 @@
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
                         <property name="can_default">True</property>
+                        <property name="receives_default">False</property>
                         <property name="tooltip" translatable="yes">refresh</property>
-                        <property name="relief">GTK_RELIEF_NONE</property>
-                        <property name="response_id">0</property>
+                        <property name="relief">none</property>
                         <child>
                           <widget class="GtkImage" id="image229">
                             <property name="visible">True</property>
@@ -194,9 +179,9 @@
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
                         <property name="can_default">True</property>
+                        <property name="receives_default">False</property>
                         <property name="tooltip" translatable="yes">home</property>
-                        <property name="relief">GTK_RELIEF_NONE</property>
-                        <property name="response_id">0</property>
+                        <property name="relief">none</property>
                         <child>
                           <widget class="GtkImage" id="image190">
                             <property name="visible">True</property>
@@ -214,7 +199,7 @@
                       <widget class="GtkImage" id="image301">
                         <property name="visible">True</property>
                         <property name="stock">gtk-jump-to</property>
-                        <property name="icon_size">2</property>
+                        <property name="icon-size">2</property>
                       </widget>
                       <packing>
                         <property name="expand">False</property>
@@ -227,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>
@@ -250,8 +243,8 @@
                   <widget class="GtkScrolledWindow" id="ScrolledBrowser">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                    <property name="hscrollbar_policy">automatic</property>
+                    <property name="vscrollbar_policy">automatic</property>
                     <child>
                       <placeholder/>
                     </child>
@@ -263,17 +256,17 @@
                     <property name="label" translatable="yes">MathView</property>
                   </widget>
                   <packing>
-                    <property name="type">tab</property>
                     <property name="tab_fill">False</property>
+                    <property name="type">tab</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkScrolledWindow" id="scrolledwindow9">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="shadow_type">GTK_SHADOW_IN</property>
+                    <property name="hscrollbar_policy">automatic</property>
+                    <property name="vscrollbar_policy">automatic</property>
+                    <property name="shadow_type">in</property>
                     <child>
                       <widget class="GtkTreeView" id="whelpResultTreeview">
                         <property name="visible">True</property>
@@ -287,26 +280,26 @@
                   </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="type">tab</property>
                     <property name="position">1</property>
                     <property name="tab_fill">False</property>
+                    <property name="type">tab</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkScrolledWindow" id="scrolledwindow11">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                    <property name="hscrollbar_policy">automatic</property>
+                    <property name="vscrollbar_policy">automatic</property>
                     <child>
                       <widget class="GtkViewport" id="viewport2">
                         <property name="visible">True</property>
-                        <property name="shadow_type">GTK_SHADOW_NONE</property>
+                        <property name="shadow_type">none</property>
                         <child>
                           <widget class="GtkImage" id="BrowserImage">
                             <property name="visible">True</property>
@@ -326,17 +319,17 @@
                     <property name="label" translatable="yes">WhelpEasterEgg</property>
                   </widget>
                   <packing>
-                    <property name="type">tab</property>
                     <property name="position">2</property>
                     <property name="tab_fill">False</property>
+                    <property name="type">tab</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkScrolledWindow" id="GraphScrolledWin">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                    <property name="hscrollbar_policy">automatic</property>
+                    <property name="vscrollbar_policy">automatic</property>
                     <child>
                       <placeholder/>
                     </child>
@@ -351,150 +344,30 @@
                     <property name="label" translatable="yes">Graph</property>
                   </widget>
                   <packing>
-                    <property name="type">tab</property>
                     <property name="position">3</property>
                     <property name="tab_fill">False</property>
-                  </packing>
-                </child>
-                <child>
-                  <widget class="GtkVBox" id="vbox16">
-                    <property name="visible">True</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>
-                    </child>
-                    <child>
-                      <widget class="GtkToolbar" id="toolbar3">
-                        <property name="visible">True</property>
-                        <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem47">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsRefreshButton">
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="label">gtk-refresh</property>
-                                <property name="use_stock">True</property>
-                                <property name="response_id">0</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="homogeneous">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem48">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsUnsubscribeButton">
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="label">gtk-remove</property>
-                                <property name="use_stock">True</property>
-                                <property name="response_id">0</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="homogeneous">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkToolItem" id="toolitem49">
-                            <property name="visible">True</property>
-                            <child>
-                              <widget class="GtkButton" id="HBugsSubscribeButton">
-                                <property name="visible">True</property>
-                                <property name="can_focus">True</property>
-                                <property name="label">gtk-add</property>
-                                <property name="use_stock">True</property>
-                                <property name="response_id">0</property>
-                              </widget>
-                            </child>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="homogeneous">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="type">tab</property>
-                    <property name="position">4</property>
-                    <property name="tab_fill">False</property>
-                  </packing>
-                </child>
-                <child>
-                  <widget class="GtkScrolledWindow" id="textScrolledWin">
-                    <property name="visible">True</property>
-                    <property name="can_focus">True</property>
-                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                    <property name="vscrollbar_policy">GTK_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="type">tab</property>
-                    <property name="position">5</property>
-                    <property name="tab_fill">False</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkVBox" id="vbox20">
                     <property name="visible">True</property>
+                    <property name="orientation">vertical</property>
                     <child>
                       <widget class="GtkScrolledWindow" id="scrolledwinContent">
                         <property name="visible">True</property>
                         <property name="can_focus">True</property>
                         <property name="border_width">3</property>
-                        <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                        <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                        <property name="shadow_type">GTK_SHADOW_IN</property>
+                        <property name="hscrollbar_policy">automatic</property>
+                        <property name="vscrollbar_policy">automatic</property>
+                        <property name="shadow_type">in</property>
                         <child>
                           <placeholder/>
                         </child>
                       </widget>
+                      <packing>
+                        <property name="position">0</property>
+                      </packing>
                     </child>
                     <child>
                       <widget class="GtkHBox" id="hbox35">
@@ -504,6 +377,7 @@
                         <child>
                           <widget class="GtkVBox" id="vbox22">
                             <property name="visible">True</property>
+                            <property name="orientation">vertical</property>
                             <child>
                               <placeholder/>
                             </child>
@@ -511,6 +385,9 @@
                               <placeholder/>
                             </child>
                           </widget>
+                          <packing>
+                            <property name="position">0</property>
+                          </packing>
                         </child>
                         <child>
                           <widget class="GtkEntry" id="entrySearch">
@@ -526,7 +403,7 @@
                           <widget class="GtkButton" id="buttonSearch">
                             <property name="visible">True</property>
                             <property name="can_focus">True</property>
-                            <property name="response_id">0</property>
+                            <property name="receives_default">False</property>
                             <child>
                               <widget class="GtkAlignment" id="alignment21">
                                 <property name="visible">True</property>
@@ -544,6 +421,7 @@
                                       <packing>
                                         <property name="expand">False</property>
                                         <property name="fill">False</property>
+                                        <property name="position">0</property>
                                       </packing>
                                     </child>
                                     <child>
@@ -577,18 +455,18 @@
                     </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="type">tab</property>
-                    <property name="position">6</property>
+                    <property name="position">4</property>
                     <property name="tab_fill">False</property>
+                    <property name="type">tab</property>
                   </packing>
                 </child>
               </widget>
@@ -605,16 +483,17 @@
     <property name="title" translatable="yes">DUMMY</property>
     <property name="resizable">False</property>
     <property name="modal">True</property>
-    <property name="window_position">GTK_WIN_POS_CENTER</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="window_position">center</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="vbox">
       <widget class="GtkVBox" id="dialog-vbox1">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <child>
           <widget class="GtkLabel" id="ConfirmationDialogLabel">
             <property name="visible">True</property>
             <property name="label" translatable="yes">DUMMY</property>
-            <property name="justify">GTK_JUSTIFY_CENTER</property>
+            <property name="justify">center</property>
           </widget>
           <packing>
             <property name="expand">False</property>
@@ -625,34 +504,44 @@
         <child internal-child="action_area">
           <widget class="GtkHButtonBox" id="dialog-action_area1">
             <property name="visible">True</property>
-            <property name="layout_style">GTK_BUTTONBOX_END</property>
+            <property name="layout_style">end</property>
             <child>
               <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-6</property>
               </widget>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="ConfirmationDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="response_id">-5</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-ok</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-5</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">1</property>
               </packing>
             </child>
           </widget>
           <packing>
             <property name="expand">False</property>
-            <property name="pack_type">GTK_PACK_END</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
           </packing>
         </child>
       </widget>
@@ -661,10 +550,11 @@
   <widget class="GtkDialog" id="EmptyDialog">
     <property name="visible">True</property>
     <property name="title" translatable="yes">DUMMY</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="vbox">
       <widget class="GtkVBox" id="EmptyDialogVBox">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <child>
           <widget class="GtkLabel" id="EmptyDialogLabel">
             <property name="visible">True</property>
@@ -682,34 +572,44 @@
         <child internal-child="action_area">
           <widget class="GtkHButtonBox" id="dialog-action_area5">
             <property name="visible">True</property>
-            <property name="layout_style">GTK_BUTTONBOX_END</property>
+            <property name="layout_style">end</property>
             <child>
               <widget class="GtkButton" id="EmptyDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-6</property>
               </widget>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="EmptyDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="response_id">-5</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-ok</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-5</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">1</property>
               </packing>
             </child>
           </widget>
           <packing>
             <property name="expand">False</property>
-            <property name="pack_type">GTK_PACK_END</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
           </packing>
         </child>
       </widget>
@@ -719,15 +619,14 @@
     <property name="border_width">10</property>
     <property name="title" translatable="yes">Select File</property>
     <property name="modal">True</property>
-    <property name="window_position">GTK_WIN_POS_CENTER</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
-    <property name="show_fileops">True</property>
+    <property name="window_position">center</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="cancel_button">
       <widget class="GtkButton" id="fileSelCancelButton">
         <property name="visible">True</property>
         <property name="can_focus">True</property>
         <property name="can_default">True</property>
-        <property name="response_id">0</property>
+        <property name="receives_default">False</property>
       </widget>
     </child>
     <child internal-child="ok_button">
@@ -735,7 +634,7 @@
         <property name="visible">True</property>
         <property name="can_focus">True</property>
         <property name="can_default">True</property>
-        <property name="response_id">0</property>
+        <property name="receives_default">False</property>
       </widget>
     </child>
   </widget>
@@ -747,10 +646,10 @@
         <child>
           <widget class="GtkVBox" id="vbox8">
             <property name="visible">True</property>
+            <property name="orientation">vertical</property>
             <child>
               <widget class="GtkHandleBox" id="menuBarHandleBox">
                 <property name="visible">True</property>
-                <property name="shadow_type">GTK_SHADOW_OUT</property>
                 <child>
                   <widget class="GtkMenuBar" id="menubar1">
                     <property name="visible">True</property>
@@ -763,62 +662,38 @@
                           <widget class="GtkMenu" id="fileMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="newMenuItem">
+                                <property name="label">gtk-new</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_New</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1047">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-new</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="n" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="openMenuItem">
+                                <property name="label">gtk-open</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Open...</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1048">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-open</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="o" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="saveMenuItem">
+                                <property name="label">gtk-save</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Save</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1049">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-save</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="s" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="saveAsMenuItem">
+                                <property name="label">gtk-save-as</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Save _as ...</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="s" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1050">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-save-as</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="s" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -826,19 +701,22 @@
                                 <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>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Quit</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1052">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-quit</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="q" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                           </widget>
@@ -854,34 +732,22 @@
                           <widget class="GtkMenu" id="editMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="undoMenuItem">
+                                <property name="label">gtk-undo</property>
                                 <property name="visible">True</property>
                                 <property name="sensitive">False</property>
-                                <property name="label" translatable="yes">_Undo</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1053">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-undo</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="z" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="redoMenuItem">
+                                <property name="label">gtk-redo</property>
                                 <property name="visible">True</property>
                                 <property name="sensitive">False</property>
-                                <property name="label" translatable="yes">_Redo</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="z" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1054">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-redo</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="z" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -891,47 +757,29 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="cutMenuItem">
+                                <property name="label">gtk-cut</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Cu_t</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1055">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-cut</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="x" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="copyMenuItem">
+                                <property name="label">gtk-copy</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Copy</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1056">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-copy</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="c" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="pasteMenuItem">
+                                <property name="label">gtk-paste</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Paste</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1057">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-paste</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="v" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -959,16 +807,10 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
+                                <property name="label">gtk-delete</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Delete</property>
                                 <property name="use_underline">True</property>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1058">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-delete</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
                               </widget>
                             </child>
                             <child>
@@ -990,17 +832,11 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="findReplMenuItem">
+                                <property name="label">gtk-find-and-replace</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Find &amp; replace ...</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1059">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-find-and-replace</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="f" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -1013,7 +849,7 @@
                                 <property name="visible">True</property>
                                 <property name="label" translatable="yes">Next ligature</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="l" modifiers="GDK_MOD1_MASK" signal="activate"/>
+                                <accelerator key="l" signal="activate" modifiers="GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -1035,19 +871,21 @@
                         <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>
-                                <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
+                                <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>
-                                <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
+                                <property name="use_stock">True</property>
+                                <accelerator key="Page_Up" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -1056,19 +894,21 @@
                               </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>
-                                <accelerator key="End" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
+                                <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>
-                                <accelerator key="Home" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
+                                <property name="use_stock">True</property>
+                                <accelerator key="Home" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -1077,11 +917,12 @@
                               </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>
-                                <accelerator key="period" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
+                                <property name="use_stock">True</property>
+                                <accelerator key="period" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
                               </widget>
                             </child>
                           </widget>
@@ -1100,7 +941,7 @@
                                 <property name="visible">True</property>
                                 <property name="label" translatable="yes">New CIC _browser</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="F3" modifiers="" signal="activate"/>
+                                <accelerator key="F3" signal="activate"/>
                               </widget>
                             </child>
                             <child>
@@ -1113,7 +954,7 @@
                                 <property name="visible">True</property>
                                 <property name="label" translatable="yes">_Fullscreen</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="F11" modifiers="" signal="activate"/>
+                                <accelerator key="F11" signal="activate"/>
                               </widget>
                             </child>
                             <child>
@@ -1122,7 +963,7 @@
                                 <property name="tooltip" translatable="yes">Shows a palette with natural deduction rules</property>
                                 <property name="label" translatable="yes">Natural deduction palette</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="F2" modifiers="" signal="activate"/>
+                                <accelerator key="F2" signal="activate"/>
                               </widget>
                             </child>
                             <child>
@@ -1132,47 +973,29 @@
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
+                                <property name="label">gtk-zoom-in</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Zoom _in</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1060">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-zoom-in</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="plus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
+                                <property name="label">gtk-zoom-out</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">Zoom _out</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1061">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-zoom-out</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="minus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
+                                <property name="label">gtk-zoom-100</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Normal size</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1062">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-zoom-100</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="equal" signal="activate" modifiers="GDK_CONTROL_MASK"/>
                               </widget>
                             </child>
                             <child>
@@ -1226,17 +1049,11 @@
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkImageMenuItem" id="showUnicodeTable">
+                              <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>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="menu-item-image20">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-select-font</property>
-                                  </widget>
-                                </child>
                               </widget>
                             </child>
                           </widget>
@@ -1268,31 +1085,19 @@
                           <widget class="GtkMenu" id="helpMenu_menu">
                             <child>
                               <widget class="GtkImageMenuItem" id="contentsMenuItem">
+                                <property name="label">gtk-help</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_Contents</property>
                                 <property name="use_underline">True</property>
-                                <accelerator key="F1" modifiers="" signal="activate"/>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1063">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-help</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
+                                <accelerator key="F1" signal="activate"/>
                               </widget>
                             </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
+                                <property name="label">gtk-about</property>
                                 <property name="visible">True</property>
-                                <property name="label" translatable="yes">_About</property>
                                 <property name="use_underline">True</property>
-                                <child internal-child="image">
-                                  <widget class="GtkImage" id="image1064">
-                                    <property name="visible">True</property>
-                                    <property name="stock">gtk-about</property>
-                                    <property name="icon_size">1</property>
-                                  </widget>
-                                </child>
+                                <property name="use_stock">True</property>
                               </widget>
                             </child>
                           </widget>
@@ -1305,6 +1110,7 @@
               <packing>
                 <property name="expand">False</property>
                 <property name="fill">False</property>
+                <property name="position">0</property>
               </packing>
             </child>
             <child>
@@ -1321,11 +1127,11 @@
                         <child>
                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
                             <property name="visible">True</property>
-                            <property name="shadow_type">GTK_SHADOW_OUT</property>
-                            <property name="handle_position">GTK_POS_TOP</property>
+                            <property name="handle_position">top</property>
                             <child>
                               <widget class="GtkVBox" id="vboxTacticsPalette">
                                 <property name="visible">True</property>
+                                <property name="orientation">vertical</property>
                                 <child>
                                   <widget class="GtkExpander" id="expander1">
                                     <property name="visible">True</property>
@@ -1333,31 +1139,33 @@
                                     <child>
                                       <widget class="GtkVBox" id="vbox1">
                                         <property name="visible">True</property>
+                                        <property name="orientation">vertical</property>
                                         <child>
                                           <widget class="GtkButton" id="butImpl_intro">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label8">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Implication (&#x21D2;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
                                           </widget>
+                                          <packing>
+                                            <property name="position">0</property>
+                                          </packing>
                                         </child>
                                         <child>
                                           <widget class="GtkButton" id="butAnd_intro">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label7">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Conjunction (∧&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Conjunction (&#x2227;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1371,11 +1179,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label9">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Disjunction left (∨&lt;sub&gt;i-l&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Disjunction left (&#x2228;&lt;sub&gt;i-l&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1389,11 +1196,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label10">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Disjunction right (∨&lt;sub&gt;i-r&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Disjunction right (&#x2228;&lt;sub&gt;i-r&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1407,11 +1213,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label11">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Negation (&#xAC;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1425,11 +1230,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label12">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Top (⊤&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Top (&#x22A4;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1443,11 +1247,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label20">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Universal (&#x2200;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1461,11 +1264,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label21">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Existential (&#x2203;&lt;sub&gt;i&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1488,6 +1290,7 @@
                                   </widget>
                                   <packing>
                                     <property name="expand">False</property>
+                                    <property name="position">0</property>
                                   </packing>
                                 </child>
                                 <child>
@@ -1497,31 +1300,33 @@
                                     <child>
                                       <widget class="GtkVBox" id="vbox3">
                                         <property name="visible">True</property>
+                                        <property name="orientation">vertical</property>
                                         <child>
                                           <widget class="GtkButton" id="butImpl_elim">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label22">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Implication (&#x21D2;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
                                           </widget>
+                                          <packing>
+                                            <property name="position">0</property>
+                                          </packing>
                                         </child>
                                         <child>
                                           <widget class="GtkButton" id="butAnd_elim_left">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label23">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Conjunction left (∧&lt;sub&gt;e-l&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Conjunction left (&#x2227;&lt;sub&gt;e-l&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1535,11 +1340,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label24">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Conjunction right (∧&lt;sub&gt;e-r&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Conjunction right (&#x2227;&lt;sub&gt;e-r&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1553,11 +1357,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label27">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Disjunction (∨&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Disjunction (&#x2228;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1571,11 +1374,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label31">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Negation (&#xAC;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1589,11 +1391,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label33">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Bottom (⊥&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Bottom (&#x22A5;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1607,11 +1408,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label34">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Universal (&#x2200;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1625,11 +1425,10 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="response_id">0</property>
                                             <child>
                                               <widget class="GtkLabel" id="label35">
                                                 <property name="visible">True</property>
-                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="label" translatable="yes">Existential (&#x2203;&lt;sub&gt;e&lt;/sub&gt;)</property>
                                                 <property name="use_markup">True</property>
                                               </widget>
                                             </child>
@@ -1662,22 +1461,24 @@
                                     <child>
                                       <widget class="GtkVBox" id="vbox4">
                                         <property name="visible">True</property>
+                                        <property name="orientation">vertical</property>
                                         <child>
                                           <widget class="GtkButton" id="butRAA">
+                                            <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
-                                            <property name="response_id">0</property>
                                           </widget>
+                                          <packing>
+                                            <property name="position">0</property>
+                                          </packing>
                                         </child>
                                         <child>
                                           <widget class="GtkButton" id="butUseLemma">
+                                            <property name="label" translatable="yes">Use lemma (lem)</property>
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Use lemma (lem)</property>
-                                            <property name="response_id">0</property>
                                           </widget>
                                           <packing>
                                             <property name="position">1</property>
@@ -1685,11 +1486,10 @@
                                         </child>
                                         <child>
                                           <widget class="GtkButton" id="butDischarge">
+                                            <property name="label" translatable="yes">Discharge (discharge)</property>
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Discharge (discharge)</property>
-                                            <property name="response_id">0</property>
                                           </widget>
                                           <packing>
                                             <property name="position">2</property>
@@ -1717,19 +1517,21 @@
                           </widget>
                           <packing>
                             <property name="expand">False</property>
+                            <property name="position">0</property>
                           </packing>
                         </child>
                         <child>
                           <widget class="GtkVBox" id="vboxScript">
                             <property name="width_request">400</property>
                             <property name="visible">True</property>
+                            <property name="orientation">vertical</property>
                             <child>
                               <widget class="GtkHBox" id="hbox28">
                                 <property name="visible">True</property>
                                 <child>
                                   <widget class="GtkToolbar" id="buttonsToolbar">
                                     <property name="visible">True</property>
-                                    <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+                                    <property name="toolbar_style">both</property>
                                     <child>
                                       <widget class="GtkToolItem" id="toolitem41">
                                         <property name="visible">True</property>
@@ -1737,9 +1539,9 @@
                                           <widget class="GtkButton" id="scriptTopButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
                                             <property name="tooltip" translatable="yes">Restart</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image920">
                                                 <property name="visible">True</property>
@@ -1751,7 +1553,6 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                     <child>
@@ -1761,9 +1562,9 @@
                                           <widget class="GtkButton" id="scriptRetractButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
                                             <property name="tooltip" translatable="yes">Retract 1 phrase</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image921">
                                                 <property name="visible">True</property>
@@ -1775,7 +1576,6 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                     <child>
@@ -1785,9 +1585,9 @@
                                           <widget class="GtkButton" id="scriptJumpButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
                                             <property name="tooltip" translatable="yes">Execute until point</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image922">
                                                 <property name="visible">True</property>
@@ -1799,7 +1599,6 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                     <child>
@@ -1809,9 +1608,9 @@
                                           <widget class="GtkButton" id="scriptAdvanceButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
                                             <property name="tooltip" translatable="yes">Execute 1 phrase</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image923">
                                                 <property name="visible">True</property>
@@ -1823,7 +1622,6 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                     <child>
@@ -1833,9 +1631,9 @@
                                           <widget class="GtkButton" id="scriptBottomButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
                                             <property name="tooltip" translatable="yes">Execute all</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image924">
                                                 <property name="visible">True</property>
@@ -1847,16 +1645,18 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                   </widget>
+                                  <packing>
+                                    <property name="position">0</property>
+                                  </packing>
                                 </child>
                                 <child>
                                   <widget class="GtkToolbar" id="toolbar2">
                                     <property name="visible">True</property>
-                                    <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
-                                    <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+                                    <property name="orientation">vertical</property>
+                                    <property name="toolbar_style">both</property>
                                     <child>
                                       <widget class="GtkToolItem" id="toolitem46">
                                         <property name="visible">True</property>
@@ -1864,8 +1664,8 @@
                                           <widget class="GtkButton" id="scriptAbortButton">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
-                                            <property name="relief">GTK_RELIEF_NONE</property>
-                                            <property name="response_id">0</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="relief">none</property>
                                             <child>
                                               <widget class="GtkImage" id="image927">
                                                 <property name="visible">True</property>
@@ -1877,7 +1677,6 @@
                                       </widget>
                                       <packing>
                                         <property name="expand">False</property>
-                                        <property name="homogeneous">False</property>
                                       </packing>
                                     </child>
                                   </widget>
@@ -1890,65 +1689,30 @@
                               <packing>
                                 <property name="expand">False</property>
                                 <property name="fill">False</property>
+                                <property name="position">0</property>
                               </packing>
                             </child>
                             <child>
                               <widget class="GtkNotebook" id="scriptNotebook">
                                 <property name="visible">True</property>
                                 <property name="can_focus">True</property>
-                                <property name="tab_pos">GTK_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">GTK_POLICY_AUTOMATIC</property>
-                                    <property name="vscrollbar_policy">GTK_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="type">tab</property>
-                                    <property name="tab_fill">False</property>
                                   </packing>
                                 </child>
                                 <child>
-                                  <widget class="GtkScrolledWindow" id="scrolledwindow8">
-                                    <property name="visible">True</property>
-                                    <property name="can_focus">True</property>
-                                    <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                                    <property name="vscrollbar_policy">GTK_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="type">tab</property>
-                                    <property name="position">1</property>
-                                    <property name="tab_fill">False</property>
                                   </packing>
                                 </child>
                               </widget>
@@ -1978,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>
@@ -1991,18 +1756,21 @@
                               <widget class="GtkScrolledWindow" id="logScrolledWin">
                                 <property name="visible">True</property>
                                 <property name="can_focus">True</property>
-                                <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
-                                <property name="shadow_type">GTK_SHADOW_IN</property>
+                                <property name="hscrollbar_policy">never</property>
+                                <property name="shadow_type">in</property>
                                 <child>
                                   <widget class="GtkTextView" id="logTextView">
                                     <property name="visible">True</property>
                                     <property name="can_focus">True</property>
                                     <property name="editable">False</property>
-                                    <property name="wrap_mode">GTK_WRAP_CHAR</property>
+                                    <property name="wrap_mode">char</property>
                                     <property name="cursor_visible">False</property>
                                   </widget>
                                 </child>
                               </widget>
+                              <packing>
+                                <property name="position">0</property>
+                              </packing>
                             </child>
                           </widget>
                           <packing>
@@ -2017,6 +1785,9 @@
                       </packing>
                     </child>
                   </widget>
+                  <packing>
+                    <property name="position">0</property>
+                  </packing>
                 </child>
               </widget>
               <packing>
@@ -2031,6 +1802,9 @@
                     <property name="visible">True</property>
                     <property name="has_resize_grip">False</property>
                   </widget>
+                  <packing>
+                    <property name="position">0</property>
+                  </packing>
                 </child>
                 <child>
                   <widget class="GtkNotebook" id="HintNotebook">
@@ -2048,8 +1822,8 @@
                         <property name="label" translatable="yes">label14</property>
                       </widget>
                       <packing>
-                        <property name="type">tab</property>
                         <property name="tab_fill">False</property>
+                        <property name="type">tab</property>
                       </packing>
                     </child>
                     <child>
@@ -2067,9 +1841,9 @@
                         <property name="label" translatable="yes">label15</property>
                       </widget>
                       <packing>
-                        <property name="type">tab</property>
                         <property name="position">1</property>
                         <property name="tab_fill">False</property>
+                        <property name="type">tab</property>
                       </packing>
                     </child>
                     <child>
@@ -2087,9 +1861,9 @@
                         <property name="label" translatable="yes">label16</property>
                       </widget>
                       <packing>
-                        <property name="type">tab</property>
                         <property name="position">2</property>
                         <property name="tab_fill">False</property>
+                        <property name="type">tab</property>
                       </packing>
                     </child>
                   </widget>
@@ -2112,10 +1886,11 @@
   </widget>
   <widget class="GtkDialog" id="TextDialog">
     <property name="title" translatable="yes">DUMMY</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="vbox">
       <widget class="GtkVBox" id="vbox5">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <child>
           <widget class="GtkLabel" id="TextDialogLabel">
             <property name="visible">True</property>
@@ -2131,9 +1906,9 @@
           <widget class="GtkScrolledWindow" id="scrolledwindow2">
             <property name="visible">True</property>
             <property name="can_focus">True</property>
-            <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-            <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-            <property name="shadow_type">GTK_SHADOW_IN</property>
+            <property name="hscrollbar_policy">automatic</property>
+            <property name="vscrollbar_policy">automatic</property>
+            <property name="shadow_type">in</property>
             <child>
               <widget class="GtkTextView" id="TextDialogTextView">
                 <property name="visible">True</property>
@@ -2148,34 +1923,44 @@
         <child internal-child="action_area">
           <widget class="GtkHButtonBox" id="hbuttonbox1">
             <property name="visible">True</property>
-            <property name="layout_style">GTK_BUTTONBOX_END</property>
+            <property name="layout_style">end</property>
             <child>
               <widget class="GtkButton" id="TextDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-6</property>
               </widget>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="TextDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="response_id">-5</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-ok</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-5</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">1</property>
               </packing>
             </child>
           </widget>
           <packing>
             <property name="expand">False</property>
-            <property name="pack_type">GTK_PACK_END</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
           </packing>
         </child>
       </widget>
@@ -2185,15 +1970,17 @@
     <property name="height_request">280</property>
     <property name="title" translatable="yes">Uri choice</property>
     <property name="modal">True</property>
-    <property name="window_position">GTK_WIN_POS_CENTER</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="window_position">center</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="vbox">
       <widget class="GtkVBox" id="dialog-vbox3">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <property name="spacing">4</property>
         <child>
           <widget class="GtkVBox" id="vbox2">
             <property name="visible">True</property>
+            <property name="orientation">vertical</property>
             <property name="spacing">3</property>
             <child>
               <widget class="GtkLabel" id="UriChoiceLabel">
@@ -2203,6 +1990,7 @@
               <packing>
                 <property name="expand">False</property>
                 <property name="fill">False</property>
+                <property name="position">0</property>
               </packing>
             </child>
             <child>
@@ -2210,8 +1998,8 @@
                 <property name="width_request">400</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                <property name="hscrollbar_policy">automatic</property>
+                <property name="vscrollbar_policy">automatic</property>
                 <child>
                   <widget class="GtkTreeView" id="UriChoiceTreeView">
                     <property name="visible">True</property>
@@ -2235,13 +2023,13 @@
                   <packing>
                     <property name="expand">False</property>
                     <property name="fill">False</property>
+                    <property name="position">0</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkEntry" id="entry1">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="invisible_char">*</property>
                   </widget>
                   <packing>
                     <property name="position">1</property>
@@ -2261,23 +2049,29 @@
         <child internal-child="action_area">
           <widget class="GtkHButtonBox" id="dialog-action_area3">
             <property name="visible">True</property>
-            <property name="layout_style">GTK_BUTTONBOX_END</property>
+            <property name="layout_style">end</property>
             <child>
               <widget class="GtkButton" id="UriChoiceAbortButton">
+                <property name="label">gtk-cancel</property>
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-6</property>
               </widget>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="UriChoiceSelectedButton">
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="response_id">0</property>
+                <property name="receives_default">False</property>
                 <child>
                   <widget class="GtkAlignment" id="alignment2">
                     <property name="visible">True</property>
@@ -2295,6 +2089,7 @@
                           <packing>
                             <property name="expand">False</property>
                             <property name="fill">False</property>
+                            <property name="position">0</property>
                           </packing>
                         </child>
                         <child>
@@ -2315,32 +2110,38 @@
                 </child>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">1</property>
               </packing>
             </child>
             <child>
               <widget class="GtkButton" id="UriChoiceConstantsButton">
+                <property name="label" translatable="yes">Try Constants</property>
                 <property name="visible">True</property>
                 <property name="sensitive">False</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label" translatable="yes">Try Constants</property>
+                <property name="receives_default">False</property>
                 <property name="use_underline">True</property>
-                <property name="response_id">0</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">2</property>
               </packing>
             </child>
             <child>
               <widget class="GtkButton" id="copyButton">
+                <property name="label">gtk-copy</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-copy</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">0</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">3</property>
               </packing>
             </child>
@@ -2349,7 +2150,7 @@
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="response_id">0</property>
+                <property name="receives_default">False</property>
                 <child>
                   <widget class="GtkAlignment" id="alignment5">
                     <property name="visible">True</property>
@@ -2367,6 +2168,7 @@
                           <packing>
                             <property name="expand">False</property>
                             <property name="fill">False</property>
+                            <property name="position">0</property>
                           </packing>
                         </child>
                         <child>
@@ -2387,26 +2189,31 @@
                 </child>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">4</property>
               </packing>
             </child>
             <child>
               <widget class="GtkButton" id="uriChoiceForwardButton">
+                <property name="label">gtk-go-forward</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-go-forward</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">0</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">5</property>
               </packing>
             </child>
           </widget>
           <packing>
             <property name="expand">False</property>
-            <property name="pack_type">GTK_PACK_END</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
           </packing>
         </child>
       </widget>
@@ -2416,8 +2223,8 @@
     <property name="border_width">5</property>
     <property name="title" translatable="yes">Find &amp; Replace</property>
     <property name="resizable">False</property>
-    <property name="window_position">GTK_WIN_POS_MOUSE</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="window_position">mouse</property>
+    <property name="type_hint">dialog</property>
     <child>
       <widget class="GtkTable" id="table1">
         <property name="visible">True</property>
@@ -2455,7 +2262,6 @@
             <property name="has_focus">True</property>
             <property name="can_default">True</property>
             <property name="has_default">True</property>
-            <property name="invisible_char">*</property>
           </widget>
           <packing>
             <property name="left_attach">1</property>
@@ -2467,7 +2273,6 @@
           <widget class="GtkEntry" id="replaceEntry">
             <property name="visible">True</property>
             <property name="can_focus">True</property>
-            <property name="invisible_char">*</property>
           </widget>
           <packing>
             <property name="left_attach">1</property>
@@ -2484,6 +2289,7 @@
             <child>
               <widget class="GtkVBox" id="vbox9">
                 <property name="visible">True</property>
+                <property name="orientation">vertical</property>
                 <child>
                   <placeholder/>
                 </child>
@@ -2491,14 +2297,17 @@
                   <placeholder/>
                 </child>
               </widget>
+              <packing>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="findButton">
+                <property name="label">gtk-find</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="label">gtk-find</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">0</property>
               </widget>
               <packing>
                 <property name="expand">False</property>
@@ -2510,7 +2319,7 @@
               <widget class="GtkButton" id="findReplButton">
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="response_id">0</property>
+                <property name="receives_default">False</property>
                 <child>
                   <widget class="GtkAlignment" id="alignment13">
                     <property name="visible">True</property>
@@ -2528,6 +2337,7 @@
                           <packing>
                             <property name="expand">False</property>
                             <property name="fill">False</property>
+                            <property name="position">0</property>
                           </packing>
                         </child>
                         <child>
@@ -2555,11 +2365,11 @@
             </child>
             <child>
               <widget class="GtkButton" id="cancelButton">
+                <property name="label">gtk-cancel</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">0</property>
               </widget>
               <packing>
                 <property name="expand">False</property>
@@ -2583,13 +2393,15 @@
     <property name="height_request">400</property>
     <property name="title" translatable="yes">title</property>
     <property name="modal">True</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+    <property name="type_hint">dialog</property>
     <child internal-child="vbox">
       <widget class="GtkVBox" id="vbox14">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <child>
           <widget class="GtkVBox" id="vbox15">
             <property name="visible">True</property>
+            <property name="orientation">vertical</property>
             <child>
               <widget class="GtkLabel" id="disambiguationErrorsLabel">
                 <property name="visible">True</property>
@@ -2598,15 +2410,16 @@
               <packing>
                 <property name="expand">False</property>
                 <property name="fill">False</property>
+                <property name="position">0</property>
               </packing>
             </child>
             <child>
               <widget class="GtkScrolledWindow" id="scrolledwindow12">
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                <property name="shadow_type">GTK_SHADOW_IN</property>
+                <property name="hscrollbar_policy">automatic</property>
+                <property name="vscrollbar_policy">automatic</property>
+                <property name="shadow_type">in</property>
                 <child>
                   <widget class="GtkTreeView" id="treeview">
                     <property name="visible">True</property>
@@ -2627,23 +2440,30 @@
         <child internal-child="action_area">
           <widget class="GtkHButtonBox" id="hbuttonbox2">
             <property name="visible">True</property>
-            <property name="layout_style">GTK_BUTTONBOX_END</property>
+            <property name="layout_style">end</property>
             <child>
               <widget class="GtkButton" id="button6">
+                <property name="label">gtk-help</property>
+                <property name="response_id">-11</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-help</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-11</property>
               </widget>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="response_id">-6</property>
+                <property name="receives_default">False</property>
                 <child>
                   <widget class="GtkAlignment" id="alignment18">
                     <property name="visible">True</property>
@@ -2661,6 +2481,7 @@
                           <packing>
                             <property name="expand">False</property>
                             <property name="fill">False</property>
+                            <property name="position">0</property>
                           </packing>
                         </child>
                         <child>
@@ -2681,40 +2502,49 @@
                 </child>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">1</property>
               </packing>
             </child>
             <child>
               <widget class="GtkButton" id="disambiguationErrorsCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="response_id">-6</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
                 <property name="has_default">True</property>
-                <property name="label">gtk-cancel</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-6</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">2</property>
               </packing>
             </child>
             <child>
               <widget class="GtkButton" id="disambiguationErrorsOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="response_id">-5</property>
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
                 <property name="can_default">True</property>
-                <property name="label">gtk-ok</property>
+                <property name="receives_default">False</property>
                 <property name="use_stock">True</property>
-                <property name="response_id">-5</property>
               </widget>
               <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
                 <property name="position">3</property>
               </packing>
             </child>
           </widget>
           <packing>
             <property name="expand">False</property>
-            <property name="pack_type">GTK_PACK_END</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
           </packing>
         </child>
       </widget>
@@ -2725,11 +2555,12 @@
     <property name="height_request">400</property>
     <property name="visible">True</property>
     <property name="title" translatable="yes">Auto</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
-    <property name="gravity">GDK_GRAVITY_SOUTH_EAST</property>
+    <property name="type_hint">dialog</property>
+    <property name="gravity">south-east</property>
     <child>
       <widget class="GtkVBox" id="vbox17">
         <property name="visible">True</property>
+        <property name="orientation">vertical</property>
         <child>
           <widget class="GtkHBox" id="hbox30">
             <property name="visible">True</property>
@@ -2738,8 +2569,8 @@
               <widget class="GtkScrolledWindow" id="scrolledwindowAREA">
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
-                <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-                <property name="shadow_type">GTK_SHADOW_IN</property>
+                <property name="vscrollbar_policy">automatic</property>
+                <property name="shadow_type">in</property>
                 <child>
                   <widget class="GtkViewport" id="viewportAREA">
                     <property name="visible">True</property>
@@ -2780,15 +2611,19 @@
                   </widget>
                 </child>
               </widget>
+              <packing>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkVBox" id="vbox18">
                 <property name="visible">True</property>
+                <property name="orientation">vertical</property>
                 <child>
                   <widget class="GtkButton" id="buttonUP">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="response_id">0</property>
+                    <property name="receives_default">False</property>
                     <child>
                       <widget class="GtkAlignment" id="alignment19">
                         <property name="visible">True</property>
@@ -2806,6 +2641,7 @@
                               <packing>
                                 <property name="expand">False</property>
                                 <property name="fill">False</property>
+                                <property name="position">0</property>
                               </packing>
                             </child>
                             <child>
@@ -2824,12 +2660,15 @@
                       </widget>
                     </child>
                   </widget>
+                  <packing>
+                    <property name="position">0</property>
+                  </packing>
                 </child>
                 <child>
                   <widget class="GtkButton" id="buttonDOWN">
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
-                    <property name="response_id">0</property>
+                    <property name="receives_default">False</property>
                     <child>
                       <widget class="GtkImage" id="image1065">
                         <property name="visible">True</property>
@@ -2849,6 +2688,9 @@
               </packing>
             </child>
           </widget>
+          <packing>
+            <property name="position">0</property>
+          </packing>
         </child>
         <child>
           <widget class="GtkHSeparator" id="hseparator3">
@@ -2869,59 +2711,73 @@
                 <property name="xalign">0</property>
                 <property name="label" translatable="yes">Last:</property>
               </widget>
+              <packing>
+                <property name="position">0</property>
+              </packing>
             </child>
             <child>
               <widget class="GtkHButtonBox" id="hbuttonbox3">
                 <property name="visible">True</property>
                 <property name="border_width">4</property>
                 <property name="spacing">4</property>
-                <property name="layout_style">GTK_BUTTONBOX_END</property>
+                <property name="layout_style">end</property>
                 <child>
                   <widget class="GtkButton" id="buttonPAUSE">
+                    <property name="label">gtk-media-pause</property>
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
                     <property name="can_default">True</property>
-                    <property name="label">gtk-media-pause</property>
+                    <property name="receives_default">False</property>
                     <property name="use_stock">True</property>
-                    <property name="response_id">0</property>
                   </widget>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">0</property>
+                  </packing>
                 </child>
                 <child>
                   <widget class="GtkButton" id="buttonPLAY">
+                    <property name="label">gtk-media-play</property>
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
                     <property name="can_default">True</property>
-                    <property name="label">gtk-media-play</property>
+                    <property name="receives_default">False</property>
                     <property name="use_stock">True</property>
-                    <property name="response_id">0</property>
                   </widget>
                   <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
                     <property name="position">1</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkButton" id="buttonNEXT">
+                    <property name="label">gtk-media-next</property>
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
                     <property name="can_default">True</property>
-                    <property name="label">gtk-media-next</property>
+                    <property name="receives_default">False</property>
                     <property name="use_stock">True</property>
-                    <property name="response_id">0</property>
                   </widget>
                   <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
                     <property name="position">2</property>
                   </packing>
                 </child>
                 <child>
                   <widget class="GtkButton" id="buttonCLOSE">
+                    <property name="label">gtk-close</property>
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
                     <property name="can_default">True</property>
-                    <property name="label">gtk-close</property>
+                    <property name="receives_default">False</property>
                     <property name="use_stock">True</property>
-                    <property name="response_id">0</property>
                   </widget>
                   <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
                     <property name="position">3</property>
                   </packing>
                 </child>