helm/matita/matita.glade

   1 <?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
   2 <!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
   3
   4 <glade-interface>
   5
   6 <widget class="GtkWindow" id="MainWin">
   7   <property name="visible">True</property>
   8   <property name="title" translatable="yes">Matita</property>
   9   <property name="type">GTK_WINDOW_TOPLEVEL</property>
  10   <property name="window_position">GTK_WIN_POS_NONE</property>
  11   <property name="modal">False</property>
  12   <property name="default_width">800</property>
  13   <property name="default_height">600</property>
  14   <property name="resizable">True</property>
  15   <property name="destroy_with_parent">False</property>
  16   <property name="decorated">True</property>
  17   <property name="skip_taskbar_hint">False</property>
  18   <property name="skip_pager_hint">False</property>
  19   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
  20   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
  21
  22   <child>
  23     <widget class="GtkEventBox" id="MainWinEventBox">
  24       <property name="visible">True</property>
  25       <property name="visible_window">True</property>
  26       <property name="above_child">False</property>
  27
  28       <child>
  29         <widget class="GtkVBox" id="MainWinShape">
  30           <property name="visible">True</property>
  31           <property name="homogeneous">False</property>
  32           <property name="spacing">0</property>
  33
  34           <child>
  35             <widget class="GtkMenuBar" id="MainMenuBar">
  36               <property name="visible">True</property>
  37
  38               <child>
  39                 <widget class="GtkMenuItem" id="FileMenu">
  40                   <property name="visible">True</property>
  41                   <property name="label" translatable="yes">_File</property>
  42                   <property name="use_underline">True</property>
  43
  44                   <child>
  45                     <widget class="GtkMenu" id="FileMenu_menu">
  46
  47                       <child>
  48                         <widget class="GtkImageMenuItem" id="NewMenu">
  49                           <property name="visible">True</property>
  50                           <property name="label" translatable="yes">_New</property>
  51                           <property name="use_underline">True</property>
  52
  53                           <child internal-child="image">
  54                             <widget class="GtkImage" id="image164">
  55                               <property name="visible">True</property>
  56                               <property name="stock">gtk-new</property>
  57                               <property name="icon_size">1</property>
  58                               <property name="xalign">0.5</property>
  59                               <property name="yalign">0.5</property>
  60                               <property name="xpad">0</property>
  61                               <property name="ypad">0</property>
  62                             </widget>
  63                           </child>
  64
  65                           <child>
  66                             <widget class="GtkMenu" id="NewMenu_menu">
  67
  68                               <child>
  69                                 <widget class="GtkMenuItem" id="NewProofMenuItem">
  70                                   <property name="visible">True</property>
  71                                   <property name="label" translatable="yes">_Proof or definition ...</property>
  72                                   <property name="use_underline">True</property>
  73                                   <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
  74                                 </widget>
  75                               </child>
  76
  77                               <child>
  78                                 <widget class="GtkMenuItem" id="NewDefsMenuItem">
  79                                   <property name="visible">True</property>
  80                                   <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
  81                                   <property name="use_underline">True</property>
  82                                 </widget>
  83                               </child>
  84                             </widget>
  85                           </child>
  86                         </widget>
  87                       </child>
  88
  89                       <child>
  90                         <widget class="GtkImageMenuItem" id="OpenMenuItem">
  91                           <property name="visible">True</property>
  92                           <property name="label" translatable="yes">_Open...</property>
  93                           <property name="use_underline">True</property>
  94                           <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
  95
  96                           <child internal-child="image">
  97                             <widget class="GtkImage" id="image165">
  98                               <property name="visible">True</property>
  99                               <property name="stock">gtk-open</property>
 100                               <property name="icon_size">1</property>
 101                               <property name="xalign">0.5</property>
 102                               <property name="yalign">0.5</property>
 103                               <property name="xpad">0</property>
 104                               <property name="ypad">0</property>
 105                             </widget>
 106                           </child>
 107                         </widget>
 108                       </child>
 109
 110                       <child>
 111                         <widget class="GtkImageMenuItem" id="SaveMenuItem">
 112                           <property name="visible">True</property>
 113                           <property name="label" translatable="yes">_Save</property>
 114                           <property name="use_underline">True</property>
 115                           <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 116
 117                           <child internal-child="image">
 118                             <widget class="GtkImage" id="image166">
 119                               <property name="visible">True</property>
 120                               <property name="stock">gtk-save</property>
 121                               <property name="icon_size">1</property>
 122                               <property name="xalign">0.5</property>
 123                               <property name="yalign">0.5</property>
 124                               <property name="xpad">0</property>
 125                               <property name="ypad">0</property>
 126                             </widget>
 127                           </child>
 128                         </widget>
 129                       </child>
 130
 131                       <child>
 132                         <widget class="GtkImageMenuItem" id="SaveAsMenuItem">
 133                           <property name="visible">True</property>
 134                           <property name="label" translatable="yes">Save _As ...</property>
 135                           <property name="use_underline">True</property>
 136
 137                           <child internal-child="image">
 138                             <widget class="GtkImage" id="image167">
 139                               <property name="visible">True</property>
 140                               <property name="stock">gtk-save-as</property>
 141                               <property name="icon_size">1</property>
 142                               <property name="xalign">0.5</property>
 143                               <property name="yalign">0.5</property>
 144                               <property name="xpad">0</property>
 145                               <property name="ypad">0</property>
 146                             </widget>
 147                           </child>
 148                         </widget>
 149                       </child>
 150
 151                       <child>
 152                         <widget class="GtkSeparatorMenuItem" id="separator1">
 153                           <property name="visible">True</property>
 154                         </widget>
 155                       </child>
 156
 157                       <child>
 158                         <widget class="GtkImageMenuItem" id="QuitMenuItem">
 159                           <property name="visible">True</property>
 160                           <property name="label" translatable="yes">_Quit</property>
 161                           <property name="use_underline">True</property>
 162                           <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 163
 164                           <child internal-child="image">
 165                             <widget class="GtkImage" id="image168">
 166                               <property name="visible">True</property>
 167                               <property name="stock">gtk-quit</property>
 168                               <property name="icon_size">1</property>
 169                               <property name="xalign">0.5</property>
 170                               <property name="yalign">0.5</property>
 171                               <property name="xpad">0</property>
 172                               <property name="ypad">0</property>
 173                             </widget>
 174                           </child>
 175                         </widget>
 176                       </child>
 177                     </widget>
 178                   </child>
 179                 </widget>
 180               </child>
 181
 182               <child>
 183                 <widget class="GtkMenuItem" id="EditMenu">
 184                   <property name="visible">True</property>
 185                   <property name="label" translatable="yes">_Edit</property>
 186                   <property name="use_underline">True</property>
 187                 </widget>
 188               </child>
 189
 190               <child>
 191                 <widget class="GtkMenuItem" id="ViewMenu">
 192                   <property name="visible">True</property>
 193                   <property name="label" translatable="yes">_View</property>
 194                   <property name="use_underline">True</property>
 195
 196                   <child>
 197                     <widget class="GtkMenu" id="ViewMenu_menu">
 198
 199                       <child>
 200                         <widget class="GtkCheckMenuItem" id="ShowToolBarMenuItem">
 201                           <property name="visible">True</property>
 202                           <property name="label" translatable="yes">Show Button Bar</property>
 203                           <property name="use_underline">True</property>
 204                           <property name="active">True</property>
 205                         </widget>
 206                       </child>
 207
 208                       <child>
 209                         <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
 210                           <property name="visible">True</property>
 211                           <property name="label" translatable="yes">Show Proof Window</property>
 212                           <property name="use_underline">True</property>
 213                           <property name="active">False</property>
 214                           <accelerator key="F3" modifiers="0" signal="activate"/>
 215                         </widget>
 216                       </child>
 217
 218                       <child>
 219                         <widget class="GtkCheckMenuItem" id="ShowCheckMenuItem">
 220                           <property name="visible">True</property>
 221                           <property name="label" translatable="yes">Show Check Window</property>
 222                           <property name="use_underline">True</property>
 223                           <property name="active">False</property>
 224                           <accelerator key="F4" modifiers="0" signal="activate"/>
 225                         </widget>
 226                       </child>
 227
 228                       <child>
 229                         <widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
 230                           <property name="visible">True</property>
 231                           <property name="label" translatable="yes">Show Script Window</property>
 232                           <property name="use_underline">True</property>
 233                           <property name="active">False</property>
 234                           <accelerator key="F5" modifiers="0" signal="activate"/>
 235                         </widget>
 236                       </child>
 237
 238                       <child>
 239                         <widget class="GtkSeparatorMenuItem" id="separator3">
 240                           <property name="visible">True</property>
 241                         </widget>
 242                       </child>
 243
 244                       <child>
 245                         <widget class="GtkMenuItem" id="ShowConsoleMenuItem">
 246                           <property name="visible">True</property>
 247                           <property name="label" translatable="yes">Show console</property>
 248                           <property name="use_underline">True</property>
 249                           <accelerator key="x" modifiers="GDK_MOD1_MASK" signal="activate"/>
 250                         </widget>
 251                       </child>
 252                     </widget>
 253                   </child>
 254                 </widget>
 255               </child>
 256
 257               <child>
 258                 <widget class="GtkMenuItem" id="DebugMenu">
 259                   <property name="visible">True</property>
 260                   <property name="label" translatable="yes">Debug</property>
 261                   <property name="use_underline">True</property>
 262
 263                   <child>
 264                     <widget class="GtkMenu" id="DebugMenu_menu">
 265
 266                       <child>
 267                         <widget class="GtkSeparatorMenuItem" id="separator2">
 268                           <property name="visible">True</property>
 269                         </widget>
 270                       </child>
 271                     </widget>
 272                   </child>
 273                 </widget>
 274               </child>
 275
 276               <child>
 277                 <widget class="GtkMenuItem" id="HelpMenu">
 278                   <property name="visible">True</property>
 279                   <property name="label" translatable="yes">_Help</property>
 280                   <property name="use_underline">True</property>
 281
 282                   <child>
 283                     <widget class="GtkMenu" id="HelpMenu_menu">
 284
 285                       <child>
 286                         <widget class="GtkMenuItem" id="AboutMenuItem">
 287                           <property name="visible">True</property>
 288                           <property name="label" translatable="yes">About...</property>
 289                           <property name="use_underline">True</property>
 290                         </widget>
 291                       </child>
 292                     </widget>
 293                   </child>
 294                 </widget>
 295               </child>
 296             </widget>
 297             <packing>
 298               <property name="padding">0</property>
 299               <property name="expand">False</property>
 300               <property name="fill">False</property>
 301             </packing>
 302           </child>
 303
 304           <child>
 305             <widget class="GtkVPaned" id="MainVPanes">
 306               <property name="visible">True</property>
 307               <property name="can_focus">True</property>
 308               <property name="position">450</property>
 309
 310               <child>
 311                 <widget class="GtkNotebook" id="SequentsNotebook">
 312                   <property name="visible">True</property>
 313                   <property name="can_focus">True</property>
 314                   <property name="show_tabs">True</property>
 315                   <property name="show_border">True</property>
 316                   <property name="tab_pos">GTK_POS_TOP</property>
 317                   <property name="scrollable">False</property>
 318                   <property name="enable_popup">False</property>
 319                 </widget>
 320                 <packing>
 321                   <property name="shrink">True</property>
 322                   <property name="resize">False</property>
 323                 </packing>
 324               </child>
 325
 326               <child>
 327                 <widget class="GtkEventBox" id="ConsoleEventBox">
 328                   <property name="visible">True</property>
 329                   <property name="visible_window">True</property>
 330                   <property name="above_child">False</property>
 331
 332                   <child>
 333                     <widget class="GtkHBox" id="hbox4">
 334                       <property name="visible">True</property>
 335                       <property name="homogeneous">False</property>
 336                       <property name="spacing">0</property>
 337
 338                       <child>
 339                         <widget class="GtkVBox" id="vbox6">
 340                           <property name="visible">True</property>
 341                           <property name="homogeneous">False</property>
 342                           <property name="spacing">0</property>
 343
 344                           <child>
 345                             <widget class="GtkButton" id="HideConsoleButton">
 346                               <property name="visible">True</property>
 347                               <property name="tooltip" translatable="yes">Hide console</property>
 348                               <property name="can_focus">True</property>
 349                               <property name="relief">GTK_RELIEF_NORMAL</property>
 350                               <property name="focus_on_click">True</property>
 351
 352                               <child>
 353                                 <widget class="GtkImage" id="image169">
 354                                   <property name="visible">True</property>
 355                                   <property name="stock">gtk-close</property>
 356                                   <property name="icon_size">4</property>
 357                                   <property name="xalign">0.5</property>
 358                                   <property name="yalign">0.5</property>
 359                                   <property name="xpad">0</property>
 360                                   <property name="ypad">0</property>
 361                                 </widget>
 362                               </child>
 363                             </widget>
 364                             <packing>
 365                               <property name="padding">0</property>
 366                               <property name="expand">False</property>
 367                               <property name="fill">False</property>
 368                             </packing>
 369                           </child>
 370                         </widget>
 371                         <packing>
 372                           <property name="padding">0</property>
 373                           <property name="expand">False</property>
 374                           <property name="fill">False</property>
 375                         </packing>
 376                       </child>
 377
 378                       <child>
 379                         <widget class="GtkScrolledWindow" id="ScrolledConsole">
 380                           <property name="visible">True</property>
 381                           <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
 382                           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 383                           <property name="shadow_type">GTK_SHADOW_IN</property>
 384                           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 385
 386                           <child>
 387                             <placeholder/>
 388                           </child>
 389                         </widget>
 390                         <packing>
 391                           <property name="padding">0</property>
 392                           <property name="expand">True</property>
 393                           <property name="fill">True</property>
 394                         </packing>
 395                       </child>
 396                     </widget>
 397                   </child>
 398                 </widget>
 399                 <packing>
 400                   <property name="shrink">True</property>
 401                   <property name="resize">True</property>
 402                 </packing>
 403               </child>
 404             </widget>
 405             <packing>
 406               <property name="padding">0</property>
 407               <property name="expand">True</property>
 408               <property name="fill">True</property>
 409             </packing>
 410           </child>
 411
 412           <child>
 413             <widget class="GtkStatusbar" id="MainStatusBar">
 414               <property name="visible">True</property>
 415               <property name="has_resize_grip">True</property>
 416             </widget>
 417             <packing>
 418               <property name="padding">0</property>
 419               <property name="expand">False</property>
 420               <property name="fill">False</property>
 421             </packing>
 422           </child>
 423         </widget>
 424       </child>
 425     </widget>
 426   </child>
 427 </widget>
 428
 429 <widget class="GtkWindow" id="ProofWin">
 430   <property name="title" translatable="yes">Matita: current proof</property>
 431   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 432   <property name="window_position">GTK_WIN_POS_NONE</property>
 433   <property name="modal">False</property>
 434   <property name="default_width">700</property>
 435   <property name="default_height">525</property>
 436   <property name="resizable">True</property>
 437   <property name="destroy_with_parent">False</property>
 438   <property name="decorated">True</property>
 439   <property name="skip_taskbar_hint">False</property>
 440   <property name="skip_pager_hint">False</property>
 441   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
 442   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 443
 444   <child>
 445     <widget class="GtkEventBox" id="ProofWinEventBox">
 446       <property name="visible">True</property>
 447       <property name="visible_window">True</property>
 448       <property name="above_child">False</property>
 449
 450       <child>
 451         <widget class="GtkScrolledWindow" id="ScrolledProof">
 452           <property name="visible">True</property>
 453           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 454           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 455           <property name="shadow_type">GTK_SHADOW_IN</property>
 456           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 457
 458           <child>
 459             <placeholder/>
 460           </child>
 461         </widget>
 462       </child>
 463     </widget>
 464   </child>
 465 </widget>
 466
 467 <widget class="GtkFileSelection" id="FileSelectionWin">
 468   <property name="border_width">10</property>
 469   <property name="title" translatable="yes">Select File</property>
 470   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 471   <property name="window_position">GTK_WIN_POS_CENTER</property>
 472   <property name="modal">True</property>
 473   <property name="resizable">True</property>
 474   <property name="destroy_with_parent">False</property>
 475   <property name="decorated">True</property>
 476   <property name="skip_taskbar_hint">False</property>
 477   <property name="skip_pager_hint">False</property>
 478   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 479   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 480   <property name="show_fileops">True</property>
 481
 482   <child internal-child="cancel_button">
 483     <widget class="GtkButton" id="fileSelCancelButton">
 484       <property name="visible">True</property>
 485       <property name="can_default">True</property>
 486       <property name="can_focus">True</property>
 487       <property name="relief">GTK_RELIEF_NORMAL</property>
 488       <property name="focus_on_click">True</property>
 489     </widget>
 490   </child>
 491
 492   <child internal-child="ok_button">
 493     <widget class="GtkButton" id="fileSelOkButton">
 494       <property name="visible">True</property>
 495       <property name="can_default">True</property>
 496       <property name="can_focus">True</property>
 497       <property name="relief">GTK_RELIEF_NORMAL</property>
 498       <property name="focus_on_click">True</property>
 499     </widget>
 500   </child>
 501 </widget>
 502
 503 <widget class="GtkWindow" id="ToolBarWin">
 504   <property name="width_request">155</property>
 505   <property name="height_request">450</property>
 506   <property name="visible">True</property>
 507   <property name="title" translatable="yes">Tactics</property>
 508   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 509   <property name="window_position">GTK_WIN_POS_NONE</property>
 510   <property name="modal">False</property>
 511   <property name="resizable">False</property>
 512   <property name="destroy_with_parent">False</property>
 513   <property name="decorated">True</property>
 514   <property name="skip_taskbar_hint">False</property>
 515   <property name="skip_pager_hint">False</property>
 516   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
 517   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 518
 519   <child>
 520     <widget class="GtkEventBox" id="ToolBarEventBox">
 521       <property name="visible">True</property>
 522       <property name="visible_window">True</property>
 523       <property name="above_child">False</property>
 524
 525       <child>
 526         <widget class="GtkVBox" id="ToolBarVBox">
 527           <property name="visible">True</property>
 528           <property name="homogeneous">False</property>
 529           <property name="spacing">0</property>
 530
 531           <child>
 532             <widget class="GtkToolbar" id="toolbar2">
 533               <property name="visible">True</property>
 534               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 535               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 536               <property name="tooltips">True</property>
 537               <property name="show_arrow">True</property>
 538
 539               <child>
 540                 <widget class="GtkToolItem" id="toolitem4">
 541                   <property name="visible">True</property>
 542                   <property name="visible_horizontal">True</property>
 543                   <property name="visible_vertical">True</property>
 544                   <property name="is_important">False</property>
 545
 546                   <child>
 547                     <widget class="GtkButton" id="introsButton">
 548                       <property name="width_request">50</property>
 549                       <property name="visible">True</property>
 550                       <property name="tooltip" translatable="yes">Intros</property>
 551                       <property name="can_focus">True</property>
 552                       <property name="label" translatable="yes">intros</property>
 553                       <property name="use_underline">True</property>
 554                       <property name="relief">GTK_RELIEF_NORMAL</property>
 555                       <property name="focus_on_click">True</property>
 556                     </widget>
 557                   </child>
 558                 </widget>
 559                 <packing>
 560                   <property name="expand">False</property>
 561                   <property name="homogeneous">False</property>
 562                 </packing>
 563               </child>
 564
 565               <child>
 566                 <widget class="GtkToolItem" id="toolitem5">
 567                   <property name="visible">True</property>
 568                   <property name="visible_horizontal">True</property>
 569                   <property name="visible_vertical">True</property>
 570                   <property name="is_important">False</property>
 571
 572                   <child>
 573                     <widget class="GtkButton" id="applyButton">
 574                       <property name="width_request">50</property>
 575                       <property name="visible">True</property>
 576                       <property name="tooltip" translatable="yes">Apply</property>
 577                       <property name="can_focus">True</property>
 578                       <property name="label" translatable="yes">apply</property>
 579                       <property name="use_underline">True</property>
 580                       <property name="relief">GTK_RELIEF_NORMAL</property>
 581                       <property name="focus_on_click">True</property>
 582                     </widget>
 583                   </child>
 584                 </widget>
 585                 <packing>
 586                   <property name="expand">False</property>
 587                   <property name="homogeneous">False</property>
 588                 </packing>
 589               </child>
 590
 591               <child>
 592                 <widget class="GtkToolItem" id="toolitem6">
 593                   <property name="visible">True</property>
 594                   <property name="visible_horizontal">True</property>
 595                   <property name="visible_vertical">True</property>
 596                   <property name="is_important">False</property>
 597
 598                   <child>
 599                     <widget class="GtkButton" id="exactButton">
 600                       <property name="width_request">50</property>
 601                       <property name="visible">True</property>
 602                       <property name="tooltip" translatable="yes">Exact</property>
 603                       <property name="can_focus">True</property>
 604                       <property name="label" translatable="yes">exact</property>
 605                       <property name="use_underline">True</property>
 606                       <property name="relief">GTK_RELIEF_NORMAL</property>
 607                       <property name="focus_on_click">True</property>
 608                     </widget>
 609                   </child>
 610                 </widget>
 611                 <packing>
 612                   <property name="expand">False</property>
 613                   <property name="homogeneous">False</property>
 614                 </packing>
 615               </child>
 616             </widget>
 617             <packing>
 618               <property name="padding">0</property>
 619               <property name="expand">False</property>
 620               <property name="fill">False</property>
 621             </packing>
 622           </child>
 623
 624           <child>
 625             <widget class="GtkToolbar" id="toolbar3">
 626               <property name="visible">True</property>
 627               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 628               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 629               <property name="tooltips">True</property>
 630               <property name="show_arrow">True</property>
 631
 632               <child>
 633                 <widget class="GtkToolItem" id="toolitem7">
 634                   <property name="visible">True</property>
 635                   <property name="visible_horizontal">True</property>
 636                   <property name="visible_vertical">True</property>
 637                   <property name="is_important">False</property>
 638
 639                   <child>
 640                     <widget class="GtkButton" id="elimButton">
 641                       <property name="width_request">50</property>
 642                       <property name="visible">True</property>
 643                       <property name="tooltip" translatable="yes">Elim</property>
 644                       <property name="can_focus">True</property>
 645                       <property name="label" translatable="yes">elim</property>
 646                       <property name="use_underline">True</property>
 647                       <property name="relief">GTK_RELIEF_NORMAL</property>
 648                       <property name="focus_on_click">True</property>
 649                     </widget>
 650                   </child>
 651                 </widget>
 652                 <packing>
 653                   <property name="expand">False</property>
 654                   <property name="homogeneous">False</property>
 655                 </packing>
 656               </child>
 657
 658               <child>
 659                 <widget class="GtkToolItem" id="toolitem8">
 660                   <property name="visible">True</property>
 661                   <property name="visible_horizontal">True</property>
 662                   <property name="visible_vertical">True</property>
 663                   <property name="is_important">False</property>
 664
 665                   <child>
 666                     <widget class="GtkButton" id="elimTypeButton">
 667                       <property name="width_request">50</property>
 668                       <property name="visible">True</property>
 669                       <property name="tooltip" translatable="yes">ElimType</property>
 670                       <property name="can_focus">True</property>
 671                       <property name="label" translatable="yes">elimTy</property>
 672                       <property name="use_underline">True</property>
 673                       <property name="relief">GTK_RELIEF_NORMAL</property>
 674                       <property name="focus_on_click">True</property>
 675                     </widget>
 676                   </child>
 677                 </widget>
 678                 <packing>
 679                   <property name="expand">False</property>
 680                   <property name="homogeneous">False</property>
 681                 </packing>
 682               </child>
 683             </widget>
 684             <packing>
 685               <property name="padding">0</property>
 686               <property name="expand">False</property>
 687               <property name="fill">False</property>
 688             </packing>
 689           </child>
 690
 691           <child>
 692             <widget class="GtkToolbar" id="toolbar4">
 693               <property name="visible">True</property>
 694               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 695               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 696               <property name="tooltips">True</property>
 697               <property name="show_arrow">True</property>
 698
 699               <child>
 700                 <widget class="GtkToolItem" id="toolitem9">
 701                   <property name="visible">True</property>
 702                   <property name="visible_horizontal">True</property>
 703                   <property name="visible_vertical">True</property>
 704                   <property name="is_important">False</property>
 705
 706                   <child>
 707                     <widget class="GtkButton" id="splitButton">
 708                       <property name="width_request">50</property>
 709                       <property name="visible">True</property>
 710                       <property name="tooltip" translatable="yes">Split</property>
 711                       <property name="can_focus">True</property>
 712                       <property name="label" translatable="yes">split</property>
 713                       <property name="use_underline">True</property>
 714                       <property name="relief">GTK_RELIEF_NORMAL</property>
 715                       <property name="focus_on_click">True</property>
 716                     </widget>
 717                   </child>
 718                 </widget>
 719                 <packing>
 720                   <property name="expand">False</property>
 721                   <property name="homogeneous">False</property>
 722                 </packing>
 723               </child>
 724
 725               <child>
 726                 <widget class="GtkToolItem" id="toolitem10">
 727                   <property name="visible">True</property>
 728                   <property name="visible_horizontal">True</property>
 729                   <property name="visible_vertical">True</property>
 730                   <property name="is_important">False</property>
 731
 732                   <child>
 733                     <widget class="GtkButton" id="leftButton">
 734                       <property name="width_request">25</property>
 735                       <property name="visible">True</property>
 736                       <property name="tooltip" translatable="yes">Left</property>
 737                       <property name="can_focus">True</property>
 738                       <property name="label" translatable="yes">L</property>
 739                       <property name="use_underline">True</property>
 740                       <property name="relief">GTK_RELIEF_NORMAL</property>
 741                       <property name="focus_on_click">True</property>
 742                     </widget>
 743                   </child>
 744                 </widget>
 745                 <packing>
 746                   <property name="expand">False</property>
 747                   <property name="homogeneous">False</property>
 748                 </packing>
 749               </child>
 750
 751               <child>
 752                 <widget class="GtkToolItem" id="toolitem11">
 753                   <property name="visible">True</property>
 754                   <property name="visible_horizontal">True</property>
 755                   <property name="visible_vertical">True</property>
 756                   <property name="is_important">False</property>
 757
 758                   <child>
 759                     <widget class="GtkButton" id="rightButton">
 760                       <property name="width_request">25</property>
 761                       <property name="visible">True</property>
 762                       <property name="tooltip" translatable="yes">Right</property>
 763                       <property name="can_focus">True</property>
 764                       <property name="label" translatable="yes">R</property>
 765                       <property name="use_underline">True</property>
 766                       <property name="relief">GTK_RELIEF_NORMAL</property>
 767                       <property name="focus_on_click">True</property>
 768                     </widget>
 769                   </child>
 770                 </widget>
 771                 <packing>
 772                   <property name="expand">False</property>
 773                   <property name="homogeneous">False</property>
 774                 </packing>
 775               </child>
 776
 777               <child>
 778                 <widget class="GtkToolItem" id="toolitem12">
 779                   <property name="visible">True</property>
 780                   <property name="visible_horizontal">True</property>
 781                   <property name="visible_vertical">True</property>
 782                   <property name="is_important">False</property>
 783
 784                   <child>
 785                     <widget class="GtkButton" id="existsButton">
 786                       <property name="width_request">25</property>
 787                       <property name="visible">True</property>
 788                       <property name="tooltip" translatable="yes">Exists</property>
 789                       <property name="can_focus">True</property>
 790                       <property name="label" translatable="yes">∃</property>
 791                       <property name="use_underline">True</property>
 792                       <property name="relief">GTK_RELIEF_NORMAL</property>
 793                       <property name="focus_on_click">True</property>
 794                     </widget>
 795                   </child>
 796                 </widget>
 797                 <packing>
 798                   <property name="expand">False</property>
 799                   <property name="homogeneous">False</property>
 800                 </packing>
 801               </child>
 802             </widget>
 803             <packing>
 804               <property name="padding">0</property>
 805               <property name="expand">False</property>
 806               <property name="fill">False</property>
 807             </packing>
 808           </child>
 809
 810           <child>
 811             <widget class="GtkToolbar" id="toolbar5">
 812               <property name="visible">True</property>
 813               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 814               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 815               <property name="tooltips">True</property>
 816               <property name="show_arrow">True</property>
 817
 818               <child>
 819                 <widget class="GtkToolItem" id="toolitem14">
 820                   <property name="visible">True</property>
 821                   <property name="visible_horizontal">True</property>
 822                   <property name="visible_vertical">True</property>
 823                   <property name="is_important">False</property>
 824
 825                   <child>
 826                     <widget class="GtkButton" id="reflexivityButton">
 827                       <property name="width_request">50</property>
 828                       <property name="visible">True</property>
 829                       <property name="tooltip" translatable="yes">Reflexivity</property>
 830                       <property name="can_focus">True</property>
 831                       <property name="label" translatable="yes">refl</property>
 832                       <property name="use_underline">True</property>
 833                       <property name="relief">GTK_RELIEF_NORMAL</property>
 834                       <property name="focus_on_click">True</property>
 835                     </widget>
 836                   </child>
 837                 </widget>
 838                 <packing>
 839                   <property name="expand">False</property>
 840                   <property name="homogeneous">False</property>
 841                 </packing>
 842               </child>
 843
 844               <child>
 845                 <widget class="GtkToolItem" id="toolitem15">
 846                   <property name="visible">True</property>
 847                   <property name="visible_horizontal">True</property>
 848                   <property name="visible_vertical">True</property>
 849                   <property name="is_important">False</property>
 850
 851                   <child>
 852                     <widget class="GtkButton" id="symmetryButton">
 853                       <property name="width_request">50</property>
 854                       <property name="visible">True</property>
 855                       <property name="tooltip" translatable="yes">Symmetry</property>
 856                       <property name="can_focus">True</property>
 857                       <property name="label" translatable="yes">sym</property>
 858                       <property name="use_underline">True</property>
 859                       <property name="relief">GTK_RELIEF_NORMAL</property>
 860                       <property name="focus_on_click">True</property>
 861                     </widget>
 862                   </child>
 863                 </widget>
 864                 <packing>
 865                   <property name="expand">False</property>
 866                   <property name="homogeneous">False</property>
 867                 </packing>
 868               </child>
 869
 870               <child>
 871                 <widget class="GtkToolItem" id="toolitem16">
 872                   <property name="visible">True</property>
 873                   <property name="visible_horizontal">True</property>
 874                   <property name="visible_vertical">True</property>
 875                   <property name="is_important">False</property>
 876
 877                   <child>
 878                     <widget class="GtkButton" id="transitivityButton">
 879                       <property name="width_request">50</property>
 880                       <property name="visible">True</property>
 881                       <property name="tooltip" translatable="yes">Transitivity</property>
 882                       <property name="can_focus">True</property>
 883                       <property name="label" translatable="yes">trans</property>
 884                       <property name="use_underline">True</property>
 885                       <property name="relief">GTK_RELIEF_NORMAL</property>
 886                       <property name="focus_on_click">True</property>
 887                     </widget>
 888                   </child>
 889                 </widget>
 890                 <packing>
 891                   <property name="expand">False</property>
 892                   <property name="homogeneous">False</property>
 893                 </packing>
 894               </child>
 895             </widget>
 896             <packing>
 897               <property name="padding">0</property>
 898               <property name="expand">False</property>
 899               <property name="fill">False</property>
 900             </packing>
 901           </child>
 902
 903           <child>
 904             <widget class="GtkToolbar" id="toolbar6">
 905               <property name="visible">True</property>
 906               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 907               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 908               <property name="tooltips">True</property>
 909               <property name="show_arrow">True</property>
 910
 911               <child>
 912                 <widget class="GtkToolItem" id="toolitem17">
 913                   <property name="visible">True</property>
 914                   <property name="visible_horizontal">True</property>
 915                   <property name="visible_vertical">True</property>
 916                   <property name="is_important">False</property>
 917
 918                   <child>
 919                     <widget class="GtkButton" id="assumptionButton">
 920                       <property name="width_request">50</property>
 921                       <property name="visible">True</property>
 922                       <property name="tooltip" translatable="yes">Assumption</property>
 923                       <property name="can_focus">True</property>
 924                       <property name="label" translatable="yes">asum</property>
 925                       <property name="use_underline">True</property>
 926                       <property name="relief">GTK_RELIEF_NORMAL</property>
 927                       <property name="focus_on_click">True</property>
 928                     </widget>
 929                   </child>
 930                 </widget>
 931                 <packing>
 932                   <property name="expand">False</property>
 933                   <property name="homogeneous">False</property>
 934                 </packing>
 935               </child>
 936
 937               <child>
 938                 <widget class="GtkToolItem" id="toolitem18">
 939                   <property name="visible">True</property>
 940                   <property name="visible_horizontal">True</property>
 941                   <property name="visible_vertical">True</property>
 942                   <property name="is_important">False</property>
 943
 944                   <child>
 945                     <widget class="GtkButton" id="autoButton">
 946                       <property name="width_request">50</property>
 947                       <property name="visible">True</property>
 948                       <property name="tooltip" translatable="yes">Auto</property>
 949                       <property name="can_focus">True</property>
 950                       <property name="label" translatable="yes">auto</property>
 951                       <property name="use_underline">True</property>
 952                       <property name="relief">GTK_RELIEF_NORMAL</property>
 953                       <property name="focus_on_click">True</property>
 954                     </widget>
 955                   </child>
 956                 </widget>
 957                 <packing>
 958                   <property name="expand">False</property>
 959                   <property name="homogeneous">False</property>
 960                 </packing>
 961               </child>
 962             </widget>
 963             <packing>
 964               <property name="padding">0</property>
 965               <property name="expand">False</property>
 966               <property name="fill">False</property>
 967             </packing>
 968           </child>
 969
 970           <child>
 971             <widget class="GtkToolbar" id="toolbar7">
 972               <property name="visible">True</property>
 973               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 974               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 975               <property name="tooltips">True</property>
 976               <property name="show_arrow">True</property>
 977
 978               <child>
 979                 <widget class="GtkToolItem" id="toolitem20">
 980                   <property name="visible">True</property>
 981                   <property name="visible_horizontal">True</property>
 982                   <property name="visible_vertical">True</property>
 983                   <property name="is_important">False</property>
 984
 985                   <child>
 986                     <widget class="GtkButton" id="cutButton">
 987                       <property name="width_request">50</property>
 988                       <property name="visible">True</property>
 989                       <property name="tooltip" translatable="yes">Cut</property>
 990                       <property name="can_focus">True</property>
 991                       <property name="label" translatable="yes">cut</property>
 992                       <property name="use_underline">True</property>
 993                       <property name="relief">GTK_RELIEF_NORMAL</property>
 994                       <property name="focus_on_click">True</property>
 995                     </widget>
 996                   </child>
 997                 </widget>
 998                 <packing>
 999                   <property name="expand">False</property>
1000                   <property name="homogeneous">False</property>
1001                 </packing>
1002               </child>
1003
1004               <child>
1005                 <widget class="GtkToolItem" id="toolitem21">
1006                   <property name="visible">True</property>
1007                   <property name="visible_horizontal">True</property>
1008                   <property name="visible_vertical">True</property>
1009                   <property name="is_important">False</property>
1010
1011                   <child>
1012                     <widget class="GtkButton" id="replaceButton">
1013                       <property name="width_request">50</property>
1014                       <property name="visible">True</property>
1015                       <property name="tooltip" translatable="yes">Replace</property>
1016                       <property name="can_focus">True</property>
1017                       <property name="label" translatable="yes">repl</property>
1018                       <property name="use_underline">True</property>
1019                       <property name="relief">GTK_RELIEF_NORMAL</property>
1020                       <property name="focus_on_click">True</property>
1021                     </widget>
1022                   </child>
1023                 </widget>
1024                 <packing>
1025                   <property name="expand">False</property>
1026                   <property name="homogeneous">False</property>
1027                 </packing>
1028               </child>
1029             </widget>
1030             <packing>
1031               <property name="padding">0</property>
1032               <property name="expand">False</property>
1033               <property name="fill">False</property>
1034             </packing>
1035           </child>
1036         </widget>
1037       </child>
1038     </widget>
1039   </child>
1040 </widget>
1041
1042 <widget class="GtkDialog" id="ConfirmationDialog">
1043   <property name="title" translatable="yes">DUMMY</property>
1044   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1045   <property name="window_position">GTK_WIN_POS_CENTER</property>
1046   <property name="modal">True</property>
1047   <property name="resizable">False</property>
1048   <property name="destroy_with_parent">False</property>
1049   <property name="decorated">True</property>
1050   <property name="skip_taskbar_hint">False</property>
1051   <property name="skip_pager_hint">False</property>
1052   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1053   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1054   <property name="has_separator">True</property>
1055
1056   <child internal-child="vbox">
1057     <widget class="GtkVBox" id="dialog-vbox1">
1058       <property name="visible">True</property>
1059       <property name="homogeneous">False</property>
1060       <property name="spacing">0</property>
1061
1062       <child internal-child="action_area">
1063         <widget class="GtkHButtonBox" id="dialog-action_area1">
1064           <property name="visible">True</property>
1065           <property name="layout_style">GTK_BUTTONBOX_END</property>
1066
1067           <child>
1068             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
1069               <property name="visible">True</property>
1070               <property name="can_default">True</property>
1071               <property name="can_focus">True</property>
1072               <property name="label">gtk-cancel</property>
1073               <property name="use_stock">True</property>
1074               <property name="relief">GTK_RELIEF_NORMAL</property>
1075               <property name="focus_on_click">True</property>
1076               <property name="response_id">-6</property>
1077             </widget>
1078           </child>
1079
1080           <child>
1081             <widget class="GtkButton" id="ConfirmationDialogOkButton">
1082               <property name="visible">True</property>
1083               <property name="can_default">True</property>
1084               <property name="can_focus">True</property>
1085               <property name="label">gtk-ok</property>
1086               <property name="use_stock">True</property>
1087               <property name="relief">GTK_RELIEF_NORMAL</property>
1088               <property name="focus_on_click">True</property>
1089               <property name="response_id">-5</property>
1090             </widget>
1091           </child>
1092         </widget>
1093         <packing>
1094           <property name="padding">0</property>
1095           <property name="expand">False</property>
1096           <property name="fill">True</property>
1097           <property name="pack_type">GTK_PACK_END</property>
1098         </packing>
1099       </child>
1100
1101       <child>
1102         <widget class="GtkLabel" id="ConfirmationDialogLabel">
1103           <property name="visible">True</property>
1104           <property name="label" translatable="yes">DUMMY</property>
1105           <property name="use_underline">False</property>
1106           <property name="use_markup">False</property>
1107           <property name="justify">GTK_JUSTIFY_CENTER</property>
1108           <property name="wrap">False</property>
1109           <property name="selectable">False</property>
1110           <property name="xalign">0.5</property>
1111           <property name="yalign">0.5</property>
1112           <property name="xpad">0</property>
1113           <property name="ypad">0</property>
1114         </widget>
1115         <packing>
1116           <property name="padding">0</property>
1117           <property name="expand">False</property>
1118           <property name="fill">False</property>
1119         </packing>
1120       </child>
1121     </widget>
1122   </child>
1123 </widget>
1124
1125 <widget class="GtkDialog" id="AboutWin">
1126   <property name="title" translatable="yes">Matita: about</property>
1127   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1128   <property name="window_position">GTK_WIN_POS_CENTER</property>
1129   <property name="modal">True</property>
1130   <property name="resizable">False</property>
1131   <property name="destroy_with_parent">False</property>
1132   <property name="decorated">True</property>
1133   <property name="skip_taskbar_hint">False</property>
1134   <property name="skip_pager_hint">False</property>
1135   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1136   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1137   <property name="has_separator">True</property>
1138
1139   <child internal-child="vbox">
1140     <widget class="GtkVBox" id="dialog-vbox2">
1141       <property name="visible">True</property>
1142       <property name="homogeneous">False</property>
1143       <property name="spacing">0</property>
1144
1145       <child internal-child="action_area">
1146         <widget class="GtkHButtonBox" id="dialog-action_area2">
1147           <property name="visible">True</property>
1148           <property name="layout_style">GTK_BUTTONBOX_END</property>
1149
1150           <child>
1151             <widget class="GtkButton" id="AboutDismissButton">
1152               <property name="visible">True</property>
1153               <property name="can_default">True</property>
1154               <property name="can_focus">True</property>
1155               <property name="label">gtk-ok</property>
1156               <property name="use_stock">True</property>
1157               <property name="relief">GTK_RELIEF_NORMAL</property>
1158               <property name="focus_on_click">True</property>
1159               <property name="response_id">-5</property>
1160             </widget>
1161           </child>
1162         </widget>
1163         <packing>
1164           <property name="padding">0</property>
1165           <property name="expand">False</property>
1166           <property name="fill">True</property>
1167           <property name="pack_type">GTK_PACK_END</property>
1168         </packing>
1169       </child>
1170
1171       <child>
1172         <widget class="GtkLabel" id="AboutLabel">
1173           <property name="visible">True</property>
1174           <property name="label" translatable="yes">&lt;b&gt;Matita @VERSION@&lt;/b&gt;
1175
1176 &lt;tt&gt;http://helm.cs.unibo.it&lt;/tt&gt;
1177
1178 Copyright (C) 2004,
1179 &lt;i&gt;the HELM team&lt;/i&gt;</property>
1180           <property name="use_underline">False</property>
1181           <property name="use_markup">True</property>
1182           <property name="justify">GTK_JUSTIFY_CENTER</property>
1183           <property name="wrap">False</property>
1184           <property name="selectable">False</property>
1185           <property name="xalign">0.5</property>
1186           <property name="yalign">0.5</property>
1187           <property name="xpad">5</property>
1188           <property name="ypad">5</property>
1189         </widget>
1190         <packing>
1191           <property name="padding">0</property>
1192           <property name="expand">False</property>
1193           <property name="fill">False</property>
1194         </packing>
1195       </child>
1196     </widget>
1197   </child>
1198 </widget>
1199
1200 <widget class="GtkDialog" id="UriChoiceDialog">
1201   <property name="height_request">280</property>
1202   <property name="title" translatable="yes">Uri choice</property>
1203   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1204   <property name="window_position">GTK_WIN_POS_CENTER</property>
1205   <property name="modal">True</property>
1206   <property name="resizable">True</property>
1207   <property name="destroy_with_parent">False</property>
1208   <property name="decorated">True</property>
1209   <property name="skip_taskbar_hint">False</property>
1210   <property name="skip_pager_hint">False</property>
1211   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1212   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1213   <property name="has_separator">True</property>
1214
1215   <child internal-child="vbox">
1216     <widget class="GtkVBox" id="dialog-vbox3">
1217       <property name="visible">True</property>
1218       <property name="homogeneous">False</property>
1219       <property name="spacing">0</property>
1220
1221       <child internal-child="action_area">
1222         <widget class="GtkHButtonBox" id="dialog-action_area3">
1223           <property name="visible">True</property>
1224           <property name="layout_style">GTK_BUTTONBOX_END</property>
1225
1226           <child>
1227             <widget class="GtkButton" id="UriChoiceAbortButton">
1228               <property name="visible">True</property>
1229               <property name="can_default">True</property>
1230               <property name="can_focus">True</property>
1231               <property name="label">gtk-cancel</property>
1232               <property name="use_stock">True</property>
1233               <property name="relief">GTK_RELIEF_NORMAL</property>
1234               <property name="focus_on_click">True</property>
1235               <property name="response_id">-6</property>
1236             </widget>
1237           </child>
1238
1239           <child>
1240             <widget class="GtkButton" id="UriChoiceSelectedButton">
1241               <property name="visible">True</property>
1242               <property name="can_default">True</property>
1243               <property name="can_focus">True</property>
1244               <property name="relief">GTK_RELIEF_NORMAL</property>
1245               <property name="focus_on_click">True</property>
1246               <property name="response_id">0</property>
1247
1248               <child>
1249                 <widget class="GtkAlignment" id="alignment2">
1250                   <property name="visible">True</property>
1251                   <property name="xalign">0.5</property>
1252                   <property name="yalign">0.5</property>
1253                   <property name="xscale">0</property>
1254                   <property name="yscale">0</property>
1255                   <property name="top_padding">0</property>
1256                   <property name="bottom_padding">0</property>
1257                   <property name="left_padding">0</property>
1258                   <property name="right_padding">0</property>
1259
1260                   <child>
1261                     <widget class="GtkHBox" id="hbox3">
1262                       <property name="visible">True</property>
1263                       <property name="homogeneous">False</property>
1264                       <property name="spacing">2</property>
1265
1266                       <child>
1267                         <widget class="GtkImage" id="image19">
1268                           <property name="visible">True</property>
1269                           <property name="stock">gtk-index</property>
1270                           <property name="icon_size">4</property>
1271                           <property name="xalign">0.5</property>
1272                           <property name="yalign">0.5</property>
1273                           <property name="xpad">0</property>
1274                           <property name="ypad">0</property>
1275                         </widget>
1276                         <packing>
1277                           <property name="padding">0</property>
1278                           <property name="expand">False</property>
1279                           <property name="fill">False</property>
1280                         </packing>
1281                       </child>
1282
1283                       <child>
1284                         <widget class="GtkLabel" id="label3">
1285                           <property name="visible">True</property>
1286                           <property name="label" translatable="yes">Try _Selected</property>
1287                           <property name="use_underline">True</property>
1288                           <property name="use_markup">False</property>
1289                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1290                           <property name="wrap">False</property>
1291                           <property name="selectable">False</property>
1292                           <property name="xalign">0.5</property>
1293                           <property name="yalign">0.5</property>
1294                           <property name="xpad">0</property>
1295                           <property name="ypad">0</property>
1296                         </widget>
1297                         <packing>
1298                           <property name="padding">0</property>
1299                           <property name="expand">False</property>
1300                           <property name="fill">False</property>
1301                         </packing>
1302                       </child>
1303                     </widget>
1304                   </child>
1305                 </widget>
1306               </child>
1307             </widget>
1308           </child>
1309
1310           <child>
1311             <widget class="GtkButton" id="UriChoiceConstantsButton">
1312               <property name="visible">True</property>
1313               <property name="sensitive">False</property>
1314               <property name="can_default">True</property>
1315               <property name="can_focus">True</property>
1316               <property name="label" translatable="yes">Try Constants</property>
1317               <property name="use_underline">True</property>
1318               <property name="relief">GTK_RELIEF_NORMAL</property>
1319               <property name="focus_on_click">True</property>
1320               <property name="response_id">0</property>
1321             </widget>
1322           </child>
1323
1324           <child>
1325             <widget class="GtkButton" id="UriChoiceAutoButton">
1326               <property name="visible">True</property>
1327               <property name="can_default">True</property>
1328               <property name="can_focus">True</property>
1329               <property name="relief">GTK_RELIEF_NORMAL</property>
1330               <property name="focus_on_click">True</property>
1331               <property name="response_id">0</property>
1332
1333               <child>
1334                 <widget class="GtkAlignment" id="alignment1">
1335                   <property name="visible">True</property>
1336                   <property name="xalign">0.5</property>
1337                   <property name="yalign">0.5</property>
1338                   <property name="xscale">0</property>
1339                   <property name="yscale">0</property>
1340                   <property name="top_padding">0</property>
1341                   <property name="bottom_padding">0</property>
1342                   <property name="left_padding">0</property>
1343                   <property name="right_padding">0</property>
1344
1345                   <child>
1346                     <widget class="GtkHBox" id="hbox1">
1347                       <property name="visible">True</property>
1348                       <property name="homogeneous">False</property>
1349                       <property name="spacing">2</property>
1350
1351                       <child>
1352                         <widget class="GtkImage" id="image18">
1353                           <property name="visible">True</property>
1354                           <property name="stock">gtk-ok</property>
1355                           <property name="icon_size">4</property>
1356                           <property name="xalign">0.5</property>
1357                           <property name="yalign">0.5</property>
1358                           <property name="xpad">0</property>
1359                           <property name="ypad">0</property>
1360                         </widget>
1361                         <packing>
1362                           <property name="padding">0</property>
1363                           <property name="expand">False</property>
1364                           <property name="fill">False</property>
1365                         </packing>
1366                       </child>
1367
1368                       <child>
1369                         <widget class="GtkLabel" id="label1">
1370                           <property name="visible">True</property>
1371                           <property name="label" translatable="yes">_Auto</property>
1372                           <property name="use_underline">True</property>
1373                           <property name="use_markup">False</property>
1374                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1375                           <property name="wrap">False</property>
1376                           <property name="selectable">False</property>
1377                           <property name="xalign">0.5</property>
1378                           <property name="yalign">0.5</property>
1379                           <property name="xpad">0</property>
1380                           <property name="ypad">0</property>
1381                         </widget>
1382                         <packing>
1383                           <property name="padding">0</property>
1384                           <property name="expand">False</property>
1385                           <property name="fill">False</property>
1386                         </packing>
1387                       </child>
1388                     </widget>
1389                   </child>
1390                 </widget>
1391               </child>
1392             </widget>
1393           </child>
1394         </widget>
1395         <packing>
1396           <property name="padding">0</property>
1397           <property name="expand">False</property>
1398           <property name="fill">True</property>
1399           <property name="pack_type">GTK_PACK_END</property>
1400         </packing>
1401       </child>
1402
1403       <child>
1404         <widget class="GtkVBox" id="vbox2">
1405           <property name="visible">True</property>
1406           <property name="homogeneous">False</property>
1407           <property name="spacing">0</property>
1408
1409           <child>
1410             <widget class="GtkLabel" id="UriChoiceLabel">
1411               <property name="visible">True</property>
1412               <property name="label" translatable="yes">some informative message here ...</property>
1413               <property name="use_underline">False</property>
1414               <property name="use_markup">False</property>
1415               <property name="justify">GTK_JUSTIFY_LEFT</property>
1416               <property name="wrap">False</property>
1417               <property name="selectable">False</property>
1418               <property name="xalign">0.5</property>
1419               <property name="yalign">0.5</property>
1420               <property name="xpad">0</property>
1421               <property name="ypad">0</property>
1422             </widget>
1423             <packing>
1424               <property name="padding">0</property>
1425               <property name="expand">False</property>
1426               <property name="fill">False</property>
1427             </packing>
1428           </child>
1429
1430           <child>
1431             <widget class="GtkScrolledWindow" id="scrolledwindow1">
1432               <property name="visible">True</property>
1433               <property name="can_focus">True</property>
1434               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1435               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1436               <property name="shadow_type">GTK_SHADOW_NONE</property>
1437               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1438
1439               <child>
1440                 <widget class="GtkTreeView" id="UriChoiceTreeView">
1441                   <property name="visible">True</property>
1442                   <property name="can_focus">True</property>
1443                   <property name="headers_visible">False</property>
1444                   <property name="rules_hint">False</property>
1445                   <property name="reorderable">False</property>
1446                   <property name="enable_search">True</property>
1447                 </widget>
1448               </child>
1449             </widget>
1450             <packing>
1451               <property name="padding">0</property>
1452               <property name="expand">True</property>
1453               <property name="fill">True</property>
1454             </packing>
1455           </child>
1456
1457           <child>
1458             <widget class="GtkHBox" id="hbox2">
1459               <property name="visible">True</property>
1460               <property name="homogeneous">False</property>
1461               <property name="spacing">0</property>
1462
1463               <child>
1464                 <widget class="GtkLabel" id="label2">
1465                   <property name="visible">True</property>
1466                   <property name="label" translatable="yes">URI: </property>
1467                   <property name="use_underline">False</property>
1468                   <property name="use_markup">False</property>
1469                   <property name="justify">GTK_JUSTIFY_LEFT</property>
1470                   <property name="wrap">False</property>
1471                   <property name="selectable">False</property>
1472                   <property name="xalign">0.5</property>
1473                   <property name="yalign">0.5</property>
1474                   <property name="xpad">0</property>
1475                   <property name="ypad">0</property>
1476                 </widget>
1477                 <packing>
1478                   <property name="padding">0</property>
1479                   <property name="expand">False</property>
1480                   <property name="fill">False</property>
1481                 </packing>
1482               </child>
1483
1484               <child>
1485                 <widget class="GtkEntry" id="entry1">
1486                   <property name="visible">True</property>
1487                   <property name="can_focus">True</property>
1488                   <property name="editable">True</property>
1489                   <property name="visibility">True</property>
1490                   <property name="max_length">0</property>
1491                   <property name="text" translatable="yes"></property>
1492                   <property name="has_frame">True</property>
1493                   <property name="invisible_char">*</property>
1494                   <property name="activates_default">False</property>
1495                 </widget>
1496                 <packing>
1497                   <property name="padding">0</property>
1498                   <property name="expand">True</property>
1499                   <property name="fill">True</property>
1500                 </packing>
1501               </child>
1502             </widget>
1503             <packing>
1504               <property name="padding">0</property>
1505               <property name="expand">False</property>
1506               <property name="fill">True</property>
1507             </packing>
1508           </child>
1509         </widget>
1510         <packing>
1511           <property name="padding">0</property>
1512           <property name="expand">True</property>
1513           <property name="fill">True</property>
1514         </packing>
1515       </child>
1516     </widget>
1517   </child>
1518 </widget>
1519
1520 <widget class="GtkDialog" id="InterpChoiceDialog">
1521   <property name="height_request">200</property>
1522   <property name="title" translatable="yes">Interpretation choice</property>
1523   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1524   <property name="window_position">GTK_WIN_POS_NONE</property>
1525   <property name="modal">True</property>
1526   <property name="resizable">True</property>
1527   <property name="destroy_with_parent">False</property>
1528   <property name="decorated">True</property>
1529   <property name="skip_taskbar_hint">False</property>
1530   <property name="skip_pager_hint">False</property>
1531   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1532   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1533   <property name="has_separator">True</property>
1534
1535   <child internal-child="vbox">
1536     <widget class="GtkVBox" id="dialog-vbox4">
1537       <property name="visible">True</property>
1538       <property name="homogeneous">False</property>
1539       <property name="spacing">0</property>
1540
1541       <child internal-child="action_area">
1542         <widget class="GtkHButtonBox" id="dialog-action_area4">
1543           <property name="visible">True</property>
1544           <property name="layout_style">GTK_BUTTONBOX_END</property>
1545
1546           <child>
1547             <widget class="GtkButton" id="InterpChoiceHelpButton">
1548               <property name="visible">True</property>
1549               <property name="can_default">True</property>
1550               <property name="can_focus">True</property>
1551               <property name="label">gtk-help</property>
1552               <property name="use_stock">True</property>
1553               <property name="relief">GTK_RELIEF_NORMAL</property>
1554               <property name="focus_on_click">True</property>
1555               <property name="response_id">-11</property>
1556             </widget>
1557           </child>
1558
1559           <child>
1560             <widget class="GtkButton" id="InterpChoiceCancelButton">
1561               <property name="visible">True</property>
1562               <property name="can_default">True</property>
1563               <property name="can_focus">True</property>
1564               <property name="label">gtk-cancel</property>
1565               <property name="use_stock">True</property>
1566               <property name="relief">GTK_RELIEF_NORMAL</property>
1567               <property name="focus_on_click">True</property>
1568               <property name="response_id">-6</property>
1569             </widget>
1570           </child>
1571
1572           <child>
1573             <widget class="GtkButton" id="InterpChoiceOkButton">
1574               <property name="visible">True</property>
1575               <property name="can_default">True</property>
1576               <property name="can_focus">True</property>
1577               <property name="label">gtk-ok</property>
1578               <property name="use_stock">True</property>
1579               <property name="relief">GTK_RELIEF_NORMAL</property>
1580               <property name="focus_on_click">True</property>
1581               <property name="response_id">-5</property>
1582             </widget>
1583           </child>
1584         </widget>
1585         <packing>
1586           <property name="padding">0</property>
1587           <property name="expand">False</property>
1588           <property name="fill">True</property>
1589           <property name="pack_type">GTK_PACK_END</property>
1590         </packing>
1591       </child>
1592
1593       <child>
1594         <widget class="GtkVBox" id="vbox3">
1595           <property name="visible">True</property>
1596           <property name="homogeneous">False</property>
1597           <property name="spacing">0</property>
1598
1599           <child>
1600             <widget class="GtkLabel" id="InterpChoiceDialogLabel">
1601               <property name="visible">True</property>
1602               <property name="label" translatable="yes">some informative message here ...</property>
1603               <property name="use_underline">False</property>
1604               <property name="use_markup">False</property>
1605               <property name="justify">GTK_JUSTIFY_LEFT</property>
1606               <property name="wrap">False</property>
1607               <property name="selectable">False</property>
1608               <property name="xalign">0.5</property>
1609               <property name="yalign">0.5</property>
1610               <property name="xpad">0</property>
1611               <property name="ypad">0</property>
1612             </widget>
1613             <packing>
1614               <property name="padding">0</property>
1615               <property name="expand">False</property>
1616               <property name="fill">False</property>
1617             </packing>
1618           </child>
1619
1620           <child>
1621             <widget class="GtkScrolledWindow" id="scrolledwindow4">
1622               <property name="visible">True</property>
1623               <property name="can_focus">True</property>
1624               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1625               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1626               <property name="shadow_type">GTK_SHADOW_IN</property>
1627               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1628
1629               <child>
1630                 <widget class="GtkTreeView" id="InterpChoiceTreeView">
1631                   <property name="visible">True</property>
1632                   <property name="can_focus">True</property>
1633                   <property name="headers_visible">False</property>
1634                   <property name="rules_hint">False</property>
1635                   <property name="reorderable">False</property>
1636                   <property name="enable_search">True</property>
1637                 </widget>
1638               </child>
1639             </widget>
1640             <packing>
1641               <property name="padding">0</property>
1642               <property name="expand">True</property>
1643               <property name="fill">True</property>
1644             </packing>
1645           </child>
1646         </widget>
1647         <packing>
1648           <property name="padding">0</property>
1649           <property name="expand">True</property>
1650           <property name="fill">True</property>
1651         </packing>
1652       </child>
1653     </widget>
1654   </child>
1655 </widget>
1656
1657 <widget class="GtkDialog" id="EmptyDialog">
1658   <property name="visible">True</property>
1659   <property name="title" translatable="yes">DUMMY</property>
1660   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1661   <property name="window_position">GTK_WIN_POS_NONE</property>
1662   <property name="modal">False</property>
1663   <property name="resizable">True</property>
1664   <property name="destroy_with_parent">False</property>
1665   <property name="decorated">True</property>
1666   <property name="skip_taskbar_hint">False</property>
1667   <property name="skip_pager_hint">False</property>
1668   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1669   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1670   <property name="has_separator">True</property>
1671
1672   <child internal-child="vbox">
1673     <widget class="GtkVBox" id="EmptyDialogVBox">
1674       <property name="visible">True</property>
1675       <property name="homogeneous">False</property>
1676       <property name="spacing">0</property>
1677
1678       <child internal-child="action_area">
1679         <widget class="GtkHButtonBox" id="dialog-action_area5">
1680           <property name="visible">True</property>
1681           <property name="layout_style">GTK_BUTTONBOX_END</property>
1682
1683           <child>
1684             <widget class="GtkButton" id="EmptyDialogCancelButton">
1685               <property name="visible">True</property>
1686               <property name="can_default">True</property>
1687               <property name="can_focus">True</property>
1688               <property name="label">gtk-cancel</property>
1689               <property name="use_stock">True</property>
1690               <property name="relief">GTK_RELIEF_NORMAL</property>
1691               <property name="focus_on_click">True</property>
1692               <property name="response_id">-6</property>
1693             </widget>
1694           </child>
1695
1696           <child>
1697             <widget class="GtkButton" id="EmptyDialogOkButton">
1698               <property name="visible">True</property>
1699               <property name="can_default">True</property>
1700               <property name="can_focus">True</property>
1701               <property name="label">gtk-ok</property>
1702               <property name="use_stock">True</property>
1703               <property name="relief">GTK_RELIEF_NORMAL</property>
1704               <property name="focus_on_click">True</property>
1705               <property name="response_id">-5</property>
1706             </widget>
1707           </child>
1708         </widget>
1709         <packing>
1710           <property name="padding">0</property>
1711           <property name="expand">False</property>
1712           <property name="fill">True</property>
1713           <property name="pack_type">GTK_PACK_END</property>
1714         </packing>
1715       </child>
1716
1717       <child>
1718         <widget class="GtkLabel" id="EmptyDialogLabel">
1719           <property name="visible">True</property>
1720           <property name="label" translatable="yes">DUMMY</property>
1721           <property name="use_underline">False</property>
1722           <property name="use_markup">False</property>
1723           <property name="justify">GTK_JUSTIFY_LEFT</property>
1724           <property name="wrap">False</property>
1725           <property name="selectable">False</property>
1726           <property name="xalign">0.5</property>
1727           <property name="yalign">0.5</property>
1728           <property name="xpad">0</property>
1729           <property name="ypad">0</property>
1730         </widget>
1731         <packing>
1732           <property name="padding">0</property>
1733           <property name="expand">False</property>
1734           <property name="fill">False</property>
1735         </packing>
1736       </child>
1737
1738       <child>
1739         <placeholder/>
1740       </child>
1741     </widget>
1742   </child>
1743 </widget>
1744
1745 <widget class="GtkWindow" id="CheckWin">
1746   <property name="width_request">300</property>
1747   <property name="height_request">200</property>
1748   <property name="title" translatable="yes">Matita: check term</property>
1749   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1750   <property name="window_position">GTK_WIN_POS_NONE</property>
1751   <property name="modal">False</property>
1752   <property name="resizable">True</property>
1753   <property name="destroy_with_parent">False</property>
1754   <property name="decorated">True</property>
1755   <property name="skip_taskbar_hint">False</property>
1756   <property name="skip_pager_hint">False</property>
1757   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1758   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1759
1760   <child>
1761     <widget class="GtkEventBox" id="CheckWinEventBox">
1762       <property name="visible">True</property>
1763       <property name="visible_window">True</property>
1764       <property name="above_child">False</property>
1765
1766       <child>
1767         <widget class="GtkScrolledWindow" id="ScrolledCheck">
1768           <property name="visible">True</property>
1769           <property name="can_focus">True</property>
1770           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1771           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1772           <property name="shadow_type">GTK_SHADOW_IN</property>
1773           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1774
1775           <child>
1776             <placeholder/>
1777           </child>
1778         </widget>
1779       </child>
1780     </widget>
1781   </child>
1782 </widget>
1783
1784 <widget class="GtkWindow" id="ScriptWin">
1785   <property name="title" translatable="yes">Matita: script</property>
1786   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1787   <property name="window_position">GTK_WIN_POS_NONE</property>
1788   <property name="modal">False</property>
1789   <property name="default_width">450</property>
1790   <property name="default_height">800</property>
1791   <property name="resizable">True</property>
1792   <property name="destroy_with_parent">False</property>
1793   <property name="decorated">True</property>
1794   <property name="skip_taskbar_hint">False</property>
1795   <property name="skip_pager_hint">False</property>
1796   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1797   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1798
1799   <child>
1800     <widget class="GtkEventBox" id="ScriptWinEventBox">
1801       <property name="visible">True</property>
1802       <property name="visible_window">True</property>
1803       <property name="above_child">False</property>
1804
1805       <child>
1806         <widget class="GtkNotebook" id="scriptNotebook">
1807           <property name="visible">True</property>
1808           <property name="can_focus">True</property>
1809           <property name="show_tabs">True</property>
1810           <property name="show_border">True</property>
1811           <property name="tab_pos">GTK_POS_BOTTOM</property>
1812           <property name="scrollable">False</property>
1813           <property name="enable_popup">False</property>
1814
1815           <child>
1816             <widget class="GtkVBox" id="vbox4">
1817               <property name="visible">True</property>
1818               <property name="homogeneous">False</property>
1819               <property name="spacing">0</property>
1820
1821               <child>
1822                 <widget class="GtkToolbar" id="toolbar1">
1823                   <property name="visible">True</property>
1824                   <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1825                   <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1826                   <property name="tooltips">True</property>
1827                   <property name="show_arrow">True</property>
1828
1829                   <child>
1830                     <widget class="GtkToolItem" id="toolitem1">
1831                       <property name="visible">True</property>
1832                       <property name="visible_horizontal">True</property>
1833                       <property name="visible_vertical">True</property>
1834                       <property name="is_important">False</property>
1835
1836                       <child>
1837                         <widget class="GtkButton" id="ScriptWinBackButton">
1838                           <property name="visible">True</property>
1839                           <property name="tooltip" translatable="yes">go back 1 phrase</property>
1840                           <property name="can_focus">True</property>
1841                           <property name="relief">GTK_RELIEF_NORMAL</property>
1842                           <property name="focus_on_click">True</property>
1843
1844                           <child>
1845                             <widget class="GtkImage" id="image133">
1846                               <property name="visible">True</property>
1847                               <property name="stock">gtk-go-back</property>
1848                               <property name="icon_size">4</property>
1849                               <property name="xalign">0.5</property>
1850                               <property name="yalign">0.5</property>
1851                               <property name="xpad">0</property>
1852                               <property name="ypad">0</property>
1853                             </widget>
1854                           </child>
1855                         </widget>
1856                       </child>
1857                     </widget>
1858                     <packing>
1859                       <property name="expand">False</property>
1860                       <property name="homogeneous">False</property>
1861                     </packing>
1862                   </child>
1863
1864                   <child>
1865                     <widget class="GtkToolItem" id="toolitem2">
1866                       <property name="visible">True</property>
1867                       <property name="visible_horizontal">True</property>
1868                       <property name="visible_vertical">True</property>
1869                       <property name="is_important">False</property>
1870
1871                       <child>
1872                         <widget class="GtkButton" id="ScriptWinJumpButton">
1873                           <property name="visible">True</property>
1874                           <property name="tooltip" translatable="yes">execute til cursor</property>
1875                           <property name="can_focus">True</property>
1876                           <property name="relief">GTK_RELIEF_NORMAL</property>
1877                           <property name="focus_on_click">True</property>
1878
1879                           <child>
1880                             <widget class="GtkImage" id="image134">
1881                               <property name="visible">True</property>
1882                               <property name="stock">gtk-jump-to</property>
1883                               <property name="icon_size">4</property>
1884                               <property name="xalign">0.5</property>
1885                               <property name="yalign">0.5</property>
1886                               <property name="xpad">0</property>
1887                               <property name="ypad">0</property>
1888                             </widget>
1889                           </child>
1890                         </widget>
1891                       </child>
1892                     </widget>
1893                     <packing>
1894                       <property name="expand">False</property>
1895                       <property name="homogeneous">False</property>
1896                     </packing>
1897                   </child>
1898
1899                   <child>
1900                     <widget class="GtkToolItem" id="toolitem3">
1901                       <property name="visible">True</property>
1902                       <property name="visible_horizontal">True</property>
1903                       <property name="visible_vertical">True</property>
1904                       <property name="is_important">False</property>
1905
1906                       <child>
1907                         <widget class="GtkButton" id="ScriptWinForwardButton">
1908                           <property name="visible">True</property>
1909                           <property name="tooltip" translatable="yes">go forward 1 phrase</property>
1910                           <property name="can_focus">True</property>
1911                           <property name="relief">GTK_RELIEF_NORMAL</property>
1912                           <property name="focus_on_click">True</property>
1913
1914                           <child>
1915                             <widget class="GtkImage" id="image135">
1916                               <property name="visible">True</property>
1917                               <property name="stock">gtk-go-forward</property>
1918                               <property name="icon_size">4</property>
1919                               <property name="xalign">0.5</property>
1920                               <property name="yalign">0.5</property>
1921                               <property name="xpad">0</property>
1922                               <property name="ypad">0</property>
1923                             </widget>
1924                           </child>
1925                         </widget>
1926                       </child>
1927                     </widget>
1928                     <packing>
1929                       <property name="expand">False</property>
1930                       <property name="homogeneous">False</property>
1931                     </packing>
1932                   </child>
1933                 </widget>
1934                 <packing>
1935                   <property name="padding">0</property>
1936                   <property name="expand">False</property>
1937                   <property name="fill">False</property>
1938                 </packing>
1939               </child>
1940
1941               <child>
1942                 <widget class="GtkScrolledWindow" id="ScrolledScript">
1943                   <property name="visible">True</property>
1944                   <property name="can_focus">True</property>
1945                   <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1946                   <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1947                   <property name="shadow_type">GTK_SHADOW_NONE</property>
1948                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1949
1950                   <child>
1951                     <widget class="GtkTextView" id="ScriptTextView">
1952                       <property name="visible">True</property>
1953                       <property name="can_focus">True</property>
1954                       <property name="editable">True</property>
1955                       <property name="overwrite">False</property>
1956                       <property name="accepts_tab">True</property>
1957                       <property name="justification">GTK_JUSTIFY_LEFT</property>
1958                       <property name="wrap_mode">GTK_WRAP_NONE</property>
1959                       <property name="cursor_visible">True</property>
1960                       <property name="pixels_above_lines">0</property>
1961                       <property name="pixels_below_lines">0</property>
1962                       <property name="pixels_inside_wrap">0</property>
1963                       <property name="left_margin">0</property>
1964                       <property name="right_margin">0</property>
1965                       <property name="indent">0</property>
1966                       <property name="text" translatable="yes"></property>
1967                     </widget>
1968                   </child>
1969                 </widget>
1970                 <packing>
1971                   <property name="padding">0</property>
1972                   <property name="expand">True</property>
1973                   <property name="fill">True</property>
1974                 </packing>
1975               </child>
1976             </widget>
1977             <packing>
1978               <property name="tab_expand">False</property>
1979               <property name="tab_fill">True</property>
1980             </packing>
1981           </child>
1982
1983           <child>
1984             <widget class="GtkLabel" id="label7">
1985               <property name="visible">True</property>
1986               <property name="label" translatable="yes">script</property>
1987               <property name="use_underline">False</property>
1988               <property name="use_markup">False</property>
1989               <property name="justify">GTK_JUSTIFY_LEFT</property>
1990               <property name="wrap">False</property>
1991               <property name="selectable">False</property>
1992               <property name="xalign">0.5</property>
1993               <property name="yalign">0.5</property>
1994               <property name="xpad">0</property>
1995               <property name="ypad">0</property>
1996             </widget>
1997             <packing>
1998               <property name="type">tab</property>
1999             </packing>
2000           </child>
2001
2002           <child>
2003             <widget class="GtkScrolledWindow" id="scrolledwindow3">
2004               <property name="visible">True</property>
2005               <property name="can_focus">True</property>
2006               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
2007               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2008               <property name="shadow_type">GTK_SHADOW_IN</property>
2009               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2010
2011               <child>
2012                 <widget class="GtkTreeView" id="treeview1">
2013                   <property name="visible">True</property>
2014                   <property name="can_focus">True</property>
2015                   <property name="headers_visible">False</property>
2016                   <property name="rules_hint">False</property>
2017                   <property name="reorderable">False</property>
2018                   <property name="enable_search">True</property>
2019                 </widget>
2020               </child>
2021             </widget>
2022             <packing>
2023               <property name="tab_expand">False</property>
2024               <property name="tab_fill">True</property>
2025             </packing>
2026           </child>
2027
2028           <child>
2029             <widget class="GtkLabel" id="label8">
2030               <property name="visible">True</property>
2031               <property name="label" translatable="yes">outline</property>
2032               <property name="use_underline">False</property>
2033               <property name="use_markup">False</property>
2034               <property name="justify">GTK_JUSTIFY_LEFT</property>
2035               <property name="wrap">False</property>
2036               <property name="selectable">False</property>
2037               <property name="xalign">0.5</property>
2038               <property name="yalign">0.5</property>
2039               <property name="xpad">0</property>
2040               <property name="ypad">0</property>
2041             </widget>
2042             <packing>
2043               <property name="type">tab</property>
2044             </packing>
2045           </child>
2046         </widget>
2047       </child>
2048     </widget>
2049   </child>
2050 </widget>
2051
2052 <widget class="GtkDialog" id="TextDialog">
2053   <property name="title" translatable="yes">DUMMY</property>
2054   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2055   <property name="window_position">GTK_WIN_POS_NONE</property>
2056   <property name="modal">False</property>
2057   <property name="resizable">True</property>
2058   <property name="destroy_with_parent">False</property>
2059   <property name="decorated">True</property>
2060   <property name="skip_taskbar_hint">False</property>
2061   <property name="skip_pager_hint">False</property>
2062   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2063   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2064   <property name="has_separator">True</property>
2065
2066   <child internal-child="vbox">
2067     <widget class="GtkVBox" id="vbox5">
2068       <property name="visible">True</property>
2069       <property name="homogeneous">False</property>
2070       <property name="spacing">0</property>
2071
2072       <child internal-child="action_area">
2073         <widget class="GtkHButtonBox" id="hbuttonbox1">
2074           <property name="visible">True</property>
2075           <property name="layout_style">GTK_BUTTONBOX_END</property>
2076
2077           <child>
2078             <widget class="GtkButton" id="TextDialogCancelButton">
2079               <property name="visible">True</property>
2080               <property name="can_default">True</property>
2081               <property name="can_focus">True</property>
2082               <property name="label">gtk-cancel</property>
2083               <property name="use_stock">True</property>
2084               <property name="relief">GTK_RELIEF_NORMAL</property>
2085               <property name="focus_on_click">True</property>
2086               <property name="response_id">-6</property>
2087             </widget>
2088           </child>
2089
2090           <child>
2091             <widget class="GtkButton" id="TextDialogOkButton">
2092               <property name="visible">True</property>
2093               <property name="can_default">True</property>
2094               <property name="can_focus">True</property>
2095               <property name="label">gtk-ok</property>
2096               <property name="use_stock">True</property>
2097               <property name="relief">GTK_RELIEF_NORMAL</property>
2098               <property name="focus_on_click">True</property>
2099               <property name="response_id">-5</property>
2100             </widget>
2101           </child>
2102         </widget>
2103         <packing>
2104           <property name="padding">0</property>
2105           <property name="expand">False</property>
2106           <property name="fill">True</property>
2107           <property name="pack_type">GTK_PACK_END</property>
2108         </packing>
2109       </child>
2110
2111       <child>
2112         <widget class="GtkLabel" id="TextDialogLabel">
2113           <property name="visible">True</property>
2114           <property name="label" translatable="yes">DUMMY</property>
2115           <property name="use_underline">False</property>
2116           <property name="use_markup">False</property>
2117           <property name="justify">GTK_JUSTIFY_LEFT</property>
2118           <property name="wrap">False</property>
2119           <property name="selectable">False</property>
2120           <property name="xalign">0.5</property>
2121           <property name="yalign">0.5</property>
2122           <property name="xpad">0</property>
2123           <property name="ypad">0</property>
2124         </widget>
2125         <packing>
2126           <property name="padding">0</property>
2127           <property name="expand">False</property>
2128           <property name="fill">False</property>
2129         </packing>
2130       </child>
2131
2132       <child>
2133         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2134           <property name="visible">True</property>
2135           <property name="can_focus">True</property>
2136           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2137           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2138           <property name="shadow_type">GTK_SHADOW_IN</property>
2139           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2140
2141           <child>
2142             <widget class="GtkTextView" id="TextDialogTextView">
2143               <property name="visible">True</property>
2144               <property name="can_focus">True</property>
2145               <property name="editable">True</property>
2146               <property name="overwrite">False</property>
2147               <property name="accepts_tab">True</property>
2148               <property name="justification">GTK_JUSTIFY_LEFT</property>
2149               <property name="wrap_mode">GTK_WRAP_NONE</property>
2150               <property name="cursor_visible">True</property>
2151               <property name="pixels_above_lines">0</property>
2152               <property name="pixels_below_lines">0</property>
2153               <property name="pixels_inside_wrap">0</property>
2154               <property name="left_margin">0</property>
2155               <property name="right_margin">0</property>
2156               <property name="indent">0</property>
2157               <property name="text" translatable="yes"></property>
2158             </widget>
2159           </child>
2160         </widget>
2161         <packing>
2162           <property name="padding">0</property>
2163           <property name="expand">True</property>
2164           <property name="fill">True</property>
2165         </packing>
2166       </child>
2167     </widget>
2168   </child>
2169 </widget>
2170
2171 </glade-interface>