]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matita.glade
*** empty log message ***
[helm.git] / helm / matita / matita.glade
index a99cb2db11ccbe96b57a1267d2b340f585981571..9c40b8efa2d0c99bd89777b014a7c4bc4580b081 100644 (file)
@@ -18,6 +18,7 @@
   <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>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkEventBox" id="BrowserWinEventBox">
                  <property name="yalign">0.5</property>
                  <property name="xpad">0</property>
                  <property name="ypad">0</property>
+                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                 <property name="width_chars">-1</property>
+                 <property name="single_line_mode">False</property>
+                 <property name="angle">0</property>
                </widget>
                <packing>
                  <property name="type">tab</property>
                      <property name="rules_hint">False</property>
                      <property name="reorderable">False</property>
                      <property name="enable_search">True</property>
+                     <property name="fixed_height_mode">False</property>
+                     <property name="hover_selection">False</property>
+                     <property name="hover_expand">False</property>
                    </widget>
                  </child>
                </widget>
                  <property name="yalign">0.5</property>
                  <property name="xpad">0</property>
                  <property name="ypad">0</property>
+                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                 <property name="width_chars">-1</property>
+                 <property name="single_line_mode">False</property>
+                 <property name="angle">0</property>
+               </widget>
+               <packing>
+                 <property name="type">tab</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkImage" id="EasterEggImage">
+                 <property name="visible">True</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xpad">0</property>
+                 <property name="ypad">0</property>
+               </widget>
+               <packing>
+                 <property name="tab_expand">False</property>
+                 <property name="tab_fill">True</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkLabel" id="EasterEggLabel">
+                 <property name="visible">True</property>
+                 <property name="label" translatable="yes">WhelpEasterEgg</property>
+                 <property name="use_underline">False</property>
+                 <property name="use_markup">False</property>
+                 <property name="justify">GTK_JUSTIFY_LEFT</property>
+                 <property name="wrap">False</property>
+                 <property name="selectable">False</property>
+                 <property name="xalign">0.5</property>
+                 <property name="yalign">0.5</property>
+                 <property name="xpad">0</property>
+                 <property name="ypad">0</property>
+                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                 <property name="width_chars">-1</property>
+                 <property name="single_line_mode">False</property>
+                 <property name="angle">0</property>
                </widget>
                <packing>
                  <property name="type">tab</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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
          <property name="yalign">0.5</property>
          <property name="xpad">0</property>
          <property name="ypad">0</property>
+         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+         <property name="width_chars">-1</property>
+         <property name="single_line_mode">False</property>
+         <property name="angle">0</property>
        </widget>
        <packing>
          <property name="padding">0</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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
          <property name="yalign">0.5</property>
          <property name="xpad">0</property>
          <property name="ypad">0</property>
+         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+         <property name="width_chars">-1</property>
+         <property name="single_line_mode">False</property>
+         <property name="angle">0</property>
        </widget>
        <packing>
          <property name="padding">0</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="focus_on_map">True</property>
   <property name="show_fileops">True</property>
 
   <child internal-child="cancel_button">
 </widget>
 
 <widget class="GtkDialog" id="InterpChoiceDialog">
-  <property name="height_request">200</property>
+  <property name="width_request">350</property>
+  <property name="height_request">250</property>
   <property name="title" translatable="yes">Interpretation choice</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_NONE</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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
              <property name="yalign">0.5</property>
              <property name="xpad">0</property>
              <property name="ypad">0</property>
+             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+             <property name="width_chars">-1</property>
+             <property name="single_line_mode">False</property>
+             <property name="angle">0</property>
            </widget>
            <packing>
              <property name="padding">0</property>
            <widget class="GtkScrolledWindow" id="scrolledwindow4">
              <property name="visible">True</property>
              <property name="can_focus">True</property>
-             <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
-             <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</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="window_placement">GTK_CORNER_TOP_LEFT</property>
 
                  <property name="rules_hint">False</property>
                  <property name="reorderable">False</property>
                  <property name="enable_search">True</property>
+                 <property name="fixed_height_mode">False</property>
+                 <property name="hover_selection">False</property>
+                 <property name="hover_expand">False</property>
                </widget>
              </child>
            </widget>
   <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>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkEventBox" id="MainWinEventBox">
                              <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="image504">
+                               <widget class="GtkImage" id="image552">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image505">
+                               <widget class="GtkImage" id="image553">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image506">
+                               <widget class="GtkImage" id="image554">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</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_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image507">
+                               <widget class="GtkImage" id="image555">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image508">
+                               <widget class="GtkImage" id="image556">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-execute</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image509">
+                               <widget class="GtkImage" id="image557">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image510">
+                               <widget class="GtkImage" id="image558">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-undo</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image511">
+                               <widget class="GtkImage" id="image559">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-redo</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image512">
+                               <widget class="GtkImage" id="image560">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-cut</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image513">
+                               <widget class="GtkImage" id="image561">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-copy</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image514">
+                               <widget class="GtkImage" id="image562">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-paste</property>
                                  <property name="icon_size">1</property>
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image515">
+                               <widget class="GtkImage" id="image563">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-delete</property>
                                  <property name="icon_size">1</property>
                            </widget>
                          </child>
 
+                         <child>
+                           <widget class="GtkMenuItem" id="selectAllMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Select _All</property>
+                             <property name="use_underline">True</property>
+                           </widget>
+                         </child>
+
+                         <child>
+                           <widget class="GtkSeparatorMenuItem" id="separator7">
+                             <property name="visible">True</property>
+                           </widget>
+                         </child>
+
                          <child>
                            <widget class="GtkImageMenuItem" id="findReplMenuItem">
                              <property name="visible">True</property>
                              <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image516">
+                               <widget class="GtkImage" id="image564">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-find-and-replace</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image517">
+                               <widget class="GtkImage" id="image565">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-in</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image518">
+                               <widget class="GtkImage" id="image566">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-out</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image519">
+                               <widget class="GtkImage" id="image567">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-100</property>
                                  <property name="icon_size">1</property>
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image520">
+                               <widget class="GtkImage" id="image568">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-about</property>
                                  <property name="icon_size">1</property>
                                  <property name="yalign">0.5</property>
                                  <property name="xpad">0</property>
                                  <property name="ypad">0</property>
+                                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                                 <property name="width_chars">-1</property>
+                                 <property name="single_line_mode">False</property>
+                                 <property name="angle">0</property>
                                </widget>
                                <packing>
                                  <property name="type">tab</property>
                                      <property name="rules_hint">False</property>
                                      <property name="reorderable">False</property>
                                      <property name="enable_search">True</property>
+                                     <property name="fixed_height_mode">False</property>
+                                     <property name="hover_selection">False</property>
+                                     <property name="hover_expand">False</property>
                                    </widget>
                                  </child>
                                </widget>
                                  <property name="yalign">0.5</property>
                                  <property name="xpad">0</property>
                                  <property name="ypad">0</property>
+                                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                                 <property name="width_chars">-1</property>
+                                 <property name="single_line_mode">False</property>
+                                 <property name="angle">0</property>
                                </widget>
                                <packing>
                                  <property name="type">tab</property>
                      <property name="yalign">0.5</property>
                      <property name="xpad">0</property>
                      <property name="ypad">0</property>
+                     <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                     <property name="width_chars">-1</property>
+                     <property name="single_line_mode">False</property>
+                     <property name="angle">0</property>
                    </widget>
                    <packing>
                      <property name="type">tab</property>
                      <property name="yalign">0.5</property>
                      <property name="xpad">0</property>
                      <property name="ypad">0</property>
+                     <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                     <property name="width_chars">-1</property>
+                     <property name="single_line_mode">False</property>
+                     <property name="angle">0</property>
                    </widget>
                    <packing>
                      <property name="type">tab</property>
                      <property name="yalign">0.5</property>
                      <property name="xpad">0</property>
                      <property name="ypad">0</property>
+                     <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                     <property name="width_chars">-1</property>
+                     <property name="single_line_mode">False</property>
+                     <property name="angle">0</property>
                    </widget>
                    <packing>
                      <property name="type">tab</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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
          <property name="yalign">0.5</property>
          <property name="xpad">0</property>
          <property name="ypad">0</property>
+         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+         <property name="width_chars">-1</property>
+         <property name="single_line_mode">False</property>
+         <property name="angle">0</property>
        </widget>
        <packing>
          <property name="padding">0</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="focus_on_map">True</property>
   <property name="has_separator">True</property>
 
   <child internal-child="vbox">
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
                        </widget>
                        <packing>
                          <property name="padding">0</property>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
                        </widget>
                        <packing>
                          <property name="padding">0</property>
              <property name="yalign">0.5</property>
              <property name="xpad">0</property>
              <property name="ypad">0</property>
+             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+             <property name="width_chars">-1</property>
+             <property name="single_line_mode">False</property>
+             <property name="angle">0</property>
            </widget>
            <packing>
              <property name="padding">0</property>
                  <property name="rules_hint">False</property>
                  <property name="reorderable">False</property>
                  <property name="enable_search">True</property>
+                 <property name="fixed_height_mode">False</property>
+                 <property name="hover_selection">False</property>
+                 <property name="hover_expand">False</property>
                </widget>
              </child>
            </widget>
                  <property name="yalign">0.5</property>
                  <property name="xpad">0</property>
                  <property name="ypad">0</property>
+                 <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                 <property name="width_chars">-1</property>
+                 <property name="single_line_mode">False</property>
+                 <property name="angle">0</property>
                </widget>
                <packing>
                  <property name="padding">0</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="focus_on_map">True</property>
 
   <child>
     <widget class="GtkTable" id="table1">
          <property name="yalign">0.5</property>
          <property name="xpad">0</property>
          <property name="ypad">0</property>
+         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+         <property name="width_chars">-1</property>
+         <property name="single_line_mode">False</property>
+         <property name="angle">0</property>
        </widget>
        <packing>
          <property name="left_attach">0</property>
          <property name="yalign">0.5</property>
          <property name="xpad">0</property>
          <property name="ypad">0</property>
+         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+         <property name="width_chars">-1</property>
+         <property name="single_line_mode">False</property>
+         <property name="angle">0</property>
        </widget>
        <packing>
          <property name="left_attach">0</property>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
                        </widget>
                        <packing>
                          <property name="padding">0</property>
   </child>
 </widget>
 
-<widget class="GtkWindow" id="newDevelopmentWin">
+<widget class="GtkWindow" id="NewDevelWin">
   <property name="title" translatable="yes">Create development</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
   <property name="skip_pager_hint">False</property>
   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkVBox" id="vbox10">
              <property name="yalign">0.5</property>
              <property name="xpad">0</property>
              <property name="ypad">0</property>
+             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+             <property name="width_chars">-1</property>
+             <property name="single_line_mode">False</property>
+             <property name="angle">0</property>
            </widget>
            <packing>
              <property name="left_attach">0</property>
              <property name="yalign">0.5</property>
              <property name="xpad">0</property>
              <property name="ypad">0</property>
+             <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+             <property name="width_chars">-1</property>
+             <property name="single_line_mode">False</property>
+             <property name="angle">0</property>
            </widget>
            <packing>
              <property name="left_attach">0</property>
   </child>
 </widget>
 
-<widget class="GtkWindow" id="develListWin">
+<widget class="GtkWindow" id="DevelListWin">
   <property name="title" translatable="yes">Developments</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_CENTER</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>
+  <property name="focus_on_map">True</property>
 
   <child>
     <widget class="GtkVBox" id="vbox12">
              <property name="rules_hint">False</property>
              <property name="reorderable">False</property>
              <property name="enable_search">True</property>
+             <property name="fixed_height_mode">False</property>
+             <property name="hover_selection">False</property>
+             <property name="hover_expand">False</property>
            </widget>
          </child>
        </widget>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
                        </widget>
                        <packing>
                          <property name="padding">0</property>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
+                         <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+                         <property name="width_chars">-1</property>
+                         <property name="single_line_mode">False</property>
+                         <property name="angle">0</property>
                        </widget>
                        <packing>
                          <property name="padding">0</property>