snapshot

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

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index de66dbf30a92cdb1a392de1a2f30e42c641f56eb..07c46bd4b6b0aab99c29fc8d447b90c1bbb8a606 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -13,6 +13,11 @@
   <property name="default_height">600</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 
   <child>
     <widget class="GtkVBox" id="MainWinShape">
@@ -328,10 +333,17 @@
   <property name="default_height">525</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 
   <child>
     <widget class="GtkEventBox" id="ProofWinEventBox">
       <property name="visible">True</property>
+      <property name="visible_window">True</property>
+      <property name="above_child">False</property>
 
       <child>
        <widget class="GtkScrolledWindow" id="ScrolledProof">
@@ -342,14 +354,7 @@
          <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
          <child>
-           <widget class="GtkViewport" id="viewport1">
-             <property name="visible">True</property>
-             <property name="shadow_type">GTK_SHADOW_IN</property>
-
-             <child>
-               <placeholder/>
-             </child>
-           </widget>
+           <placeholder/>
          </child>
        </widget>
       </child>
@@ -365,6 +370,11 @@
   <property name="modal">True</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="show_fileops">True</property>
 
   <child internal-child="cancel_button">
@@ -373,6 +383,7 @@
       <property name="can_default">True</property>
       <property name="can_focus">True</property>
       <property name="relief">GTK_RELIEF_NORMAL</property>
+      <property name="focus_on_click">True</property>
     </widget>
   </child>
 
@@ -382,6 +393,7 @@
       <property name="can_default">True</property>
       <property name="can_focus">True</property>
       <property name="relief">GTK_RELIEF_NORMAL</property>
+      <property name="focus_on_click">True</property>
     </widget>
   </child>
 </widget>
@@ -396,10 +408,17 @@
   <property name="modal">False</property>
   <property name="resizable">False</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 
   <child>
     <widget class="GtkEventBox" id="ToolBarEventBox">
       <property name="visible">True</property>
+      <property name="visible_window">True</property>
+      <property name="above_child">False</property>
 
       <child>
        <widget class="GtkVBox" id="vbox1">
@@ -422,6 +441,7 @@
                  <property name="label" translatable="yes">button1</property>
                  <property name="use_underline">True</property>
                  <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
                </widget>
              </child>
 
@@ -433,6 +453,7 @@
                  <property name="label" translatable="yes">button2</property>
                  <property name="use_underline">True</property>
                  <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
                </widget>
              </child>
 
@@ -444,6 +465,7 @@
                  <property name="label" translatable="yes">button3</property>
                  <property name="use_underline">True</property>
                  <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
                </widget>
              </child>
 
@@ -455,6 +477,7 @@
                  <property name="label" translatable="yes">button4</property>
                  <property name="use_underline">True</property>
                  <property name="relief">GTK_RELIEF_NORMAL</property>
+                 <property name="focus_on_click">True</property>
                </widget>
              </child>
            </widget>
@@ -492,6 +515,11 @@
   <property name="modal">True</property>
   <property name="resizable">False</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -513,6 +541,7 @@
              <property name="label">gtk-cancel</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-6</property>
            </widget>
          </child>
@@ -525,6 +554,7 @@
              <property name="label">gtk-ok</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-5</property>
            </widget>
          </child>
@@ -568,6 +598,11 @@
   <property name="modal">True</property>
   <property name="resizable">False</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -589,6 +624,7 @@
              <property name="label">gtk-ok</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-5</property>
            </widget>
          </child>
@@ -616,6 +652,11 @@
   <property name="modal">True</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -637,6 +678,7 @@
              <property name="label">gtk-cancel</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-6</property>
            </widget>
          </child>
@@ -647,6 +689,7 @@
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">0</property>
 
              <child>
@@ -656,6 +699,10 @@
                  <property name="yalign">0.5</property>
                  <property name="xscale">0</property>
                  <property name="yscale">0</property>
+                 <property name="top_padding">0</property>
+                 <property name="bottom_padding">0</property>
+                 <property name="left_padding">0</property>
+                 <property name="right_padding">0</property>
 
                  <child>
                    <widget class="GtkHBox" id="hbox3">
@@ -716,6 +763,7 @@
              <property name="label" translatable="yes">Try Constants</property>
              <property name="use_underline">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">0</property>
            </widget>
          </child>
@@ -726,6 +774,7 @@
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">0</property>
 
              <child>
@@ -735,6 +784,10 @@
                  <property name="yalign">0.5</property>
                  <property name="xscale">0</property>
                  <property name="yscale">0</property>
+                 <property name="top_padding">0</property>
+                 <property name="bottom_padding">0</property>
+                 <property name="left_padding">0</property>
+                 <property name="right_padding">0</property>
 
                  <child>
                    <widget class="GtkHBox" id="hbox1">
@@ -918,6 +971,11 @@
   <property name="modal">True</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -939,6 +997,7 @@
              <property name="label">gtk-help</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-11</property>
            </widget>
          </child>
@@ -951,6 +1010,7 @@
              <property name="label">gtk-cancel</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-6</property>
            </widget>
          </child>
@@ -963,6 +1023,7 @@
              <property name="label">gtk-ok</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-5</property>
            </widget>
          </child>
@@ -1024,6 +1085,11 @@
   <property name="modal">False</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
@@ -1045,6 +1111,7 @@
              <property name="label">gtk-cancel</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-6</property>
            </widget>
          </child>
@@ -1057,6 +1124,7 @@
              <property name="label">gtk-ok</property>
              <property name="use_stock">True</property>
              <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
              <property name="response_id">-5</property>
            </widget>
          </child>