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="image174">
  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="image175">
  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="image176">
 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="image177">
 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="image178">
 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">Toggle 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="ConsoleHBox">
 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_AUTOMATIC</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">False</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="toolbar8">
 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="toolitem22">
 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="simplifyButton">
 920                       <property name="width_request">50</property>
 921                       <property name="visible">True</property>
 922                       <property name="tooltip" translatable="yes">Simplify</property>
 923                       <property name="can_focus">True</property>
 924                       <property name="label" translatable="yes">simpl</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="toolitem23">
 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="reduceButton">
 946                       <property name="width_request">50</property>
 947                       <property name="visible">True</property>
 948                       <property name="tooltip" translatable="yes">Reduce</property>
 949                       <property name="can_focus">True</property>
 950                       <property name="label" translatable="yes">red</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
 963               <child>
 964                 <widget class="GtkToolItem" id="toolitem24">
 965                   <property name="visible">True</property>
 966                   <property name="visible_horizontal">True</property>
 967                   <property name="visible_vertical">True</property>
 968                   <property name="is_important">False</property>
 969
 970                   <child>
 971                     <widget class="GtkButton" id="whdButton">
 972                       <property name="width_request">50</property>
 973                       <property name="visible">True</property>
 974                       <property name="tooltip" translatable="yes">Whd</property>
 975                       <property name="can_focus">True</property>
 976                       <property name="label" translatable="yes">whd</property>
 977                       <property name="use_underline">True</property>
 978                       <property name="relief">GTK_RELIEF_NORMAL</property>
 979                       <property name="focus_on_click">True</property>
 980                     </widget>
 981                   </child>
 982                 </widget>
 983                 <packing>
 984                   <property name="expand">False</property>
 985                   <property name="homogeneous">False</property>
 986                 </packing>
 987               </child>
 988             </widget>
 989             <packing>
 990               <property name="padding">0</property>
 991               <property name="expand">False</property>
 992               <property name="fill">False</property>
 993             </packing>
 994           </child>
 995
 996           <child>
 997             <widget class="GtkToolbar" id="toolbar6">
 998               <property name="visible">True</property>
 999               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1000               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1001               <property name="tooltips">True</property>
1002               <property name="show_arrow">True</property>
1003
1004               <child>
1005                 <widget class="GtkToolItem" id="toolitem17">
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="assumptionButton">
1013                       <property name="width_request">50</property>
1014                       <property name="visible">True</property>
1015                       <property name="tooltip" translatable="yes">Assumption</property>
1016                       <property name="can_focus">True</property>
1017                       <property name="label" translatable="yes">asum</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
1030               <child>
1031                 <widget class="GtkToolItem" id="toolitem18">
1032                   <property name="visible">True</property>
1033                   <property name="visible_horizontal">True</property>
1034                   <property name="visible_vertical">True</property>
1035                   <property name="is_important">False</property>
1036
1037                   <child>
1038                     <widget class="GtkButton" id="autoButton">
1039                       <property name="width_request">50</property>
1040                       <property name="visible">True</property>
1041                       <property name="tooltip" translatable="yes">Auto</property>
1042                       <property name="can_focus">True</property>
1043                       <property name="label" translatable="yes">auto</property>
1044                       <property name="use_underline">True</property>
1045                       <property name="relief">GTK_RELIEF_NORMAL</property>
1046                       <property name="focus_on_click">True</property>
1047                     </widget>
1048                   </child>
1049                 </widget>
1050                 <packing>
1051                   <property name="expand">False</property>
1052                   <property name="homogeneous">False</property>
1053                 </packing>
1054               </child>
1055             </widget>
1056             <packing>
1057               <property name="padding">0</property>
1058               <property name="expand">False</property>
1059               <property name="fill">False</property>
1060             </packing>
1061           </child>
1062
1063           <child>
1064             <widget class="GtkToolbar" id="toolbar7">
1065               <property name="visible">True</property>
1066               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1067               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1068               <property name="tooltips">True</property>
1069               <property name="show_arrow">True</property>
1070
1071               <child>
1072                 <widget class="GtkToolItem" id="toolitem20">
1073                   <property name="visible">True</property>
1074                   <property name="visible_horizontal">True</property>
1075                   <property name="visible_vertical">True</property>
1076                   <property name="is_important">False</property>
1077
1078                   <child>
1079                     <widget class="GtkButton" id="cutButton">
1080                       <property name="width_request">50</property>
1081                       <property name="visible">True</property>
1082                       <property name="tooltip" translatable="yes">Cut</property>
1083                       <property name="can_focus">True</property>
1084                       <property name="label" translatable="yes">cut</property>
1085                       <property name="use_underline">True</property>
1086                       <property name="relief">GTK_RELIEF_NORMAL</property>
1087                       <property name="focus_on_click">True</property>
1088                     </widget>
1089                   </child>
1090                 </widget>
1091                 <packing>
1092                   <property name="expand">False</property>
1093                   <property name="homogeneous">False</property>
1094                 </packing>
1095               </child>
1096
1097               <child>
1098                 <widget class="GtkToolItem" id="toolitem21">
1099                   <property name="visible">True</property>
1100                   <property name="visible_horizontal">True</property>
1101                   <property name="visible_vertical">True</property>
1102                   <property name="is_important">False</property>
1103
1104                   <child>
1105                     <widget class="GtkButton" id="replaceButton">
1106                       <property name="width_request">50</property>
1107                       <property name="visible">True</property>
1108                       <property name="tooltip" translatable="yes">Replace</property>
1109                       <property name="can_focus">True</property>
1110                       <property name="label" translatable="yes">repl</property>
1111                       <property name="use_underline">True</property>
1112                       <property name="relief">GTK_RELIEF_NORMAL</property>
1113                       <property name="focus_on_click">True</property>
1114                     </widget>
1115                   </child>
1116                 </widget>
1117                 <packing>
1118                   <property name="expand">False</property>
1119                   <property name="homogeneous">False</property>
1120                 </packing>
1121               </child>
1122             </widget>
1123             <packing>
1124               <property name="padding">0</property>
1125               <property name="expand">False</property>
1126               <property name="fill">False</property>
1127             </packing>
1128           </child>
1129         </widget>
1130       </child>
1131     </widget>
1132   </child>
1133 </widget>
1134
1135 <widget class="GtkDialog" id="ConfirmationDialog">
1136   <property name="title" translatable="yes">DUMMY</property>
1137   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1138   <property name="window_position">GTK_WIN_POS_CENTER</property>
1139   <property name="modal">True</property>
1140   <property name="resizable">False</property>
1141   <property name="destroy_with_parent">False</property>
1142   <property name="decorated">True</property>
1143   <property name="skip_taskbar_hint">False</property>
1144   <property name="skip_pager_hint">False</property>
1145   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1146   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1147   <property name="has_separator">True</property>
1148
1149   <child internal-child="vbox">
1150     <widget class="GtkVBox" id="dialog-vbox1">
1151       <property name="visible">True</property>
1152       <property name="homogeneous">False</property>
1153       <property name="spacing">0</property>
1154
1155       <child internal-child="action_area">
1156         <widget class="GtkHButtonBox" id="dialog-action_area1">
1157           <property name="visible">True</property>
1158           <property name="layout_style">GTK_BUTTONBOX_END</property>
1159
1160           <child>
1161             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
1162               <property name="visible">True</property>
1163               <property name="can_default">True</property>
1164               <property name="can_focus">True</property>
1165               <property name="label">gtk-cancel</property>
1166               <property name="use_stock">True</property>
1167               <property name="relief">GTK_RELIEF_NORMAL</property>
1168               <property name="focus_on_click">True</property>
1169               <property name="response_id">-6</property>
1170             </widget>
1171           </child>
1172
1173           <child>
1174             <widget class="GtkButton" id="ConfirmationDialogOkButton">
1175               <property name="visible">True</property>
1176               <property name="can_default">True</property>
1177               <property name="can_focus">True</property>
1178               <property name="label">gtk-ok</property>
1179               <property name="use_stock">True</property>
1180               <property name="relief">GTK_RELIEF_NORMAL</property>
1181               <property name="focus_on_click">True</property>
1182               <property name="response_id">-5</property>
1183             </widget>
1184           </child>
1185         </widget>
1186         <packing>
1187           <property name="padding">0</property>
1188           <property name="expand">False</property>
1189           <property name="fill">True</property>
1190           <property name="pack_type">GTK_PACK_END</property>
1191         </packing>
1192       </child>
1193
1194       <child>
1195         <widget class="GtkLabel" id="ConfirmationDialogLabel">
1196           <property name="visible">True</property>
1197           <property name="label" translatable="yes">DUMMY</property>
1198           <property name="use_underline">False</property>
1199           <property name="use_markup">False</property>
1200           <property name="justify">GTK_JUSTIFY_CENTER</property>
1201           <property name="wrap">False</property>
1202           <property name="selectable">False</property>
1203           <property name="xalign">0.5</property>
1204           <property name="yalign">0.5</property>
1205           <property name="xpad">0</property>
1206           <property name="ypad">0</property>
1207         </widget>
1208         <packing>
1209           <property name="padding">0</property>
1210           <property name="expand">False</property>
1211           <property name="fill">False</property>
1212         </packing>
1213       </child>
1214     </widget>
1215   </child>
1216 </widget>
1217
1218 <widget class="GtkDialog" id="AboutWin">
1219   <property name="title" translatable="yes">Matita: about</property>
1220   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1221   <property name="window_position">GTK_WIN_POS_CENTER</property>
1222   <property name="modal">True</property>
1223   <property name="resizable">False</property>
1224   <property name="destroy_with_parent">False</property>
1225   <property name="decorated">True</property>
1226   <property name="skip_taskbar_hint">False</property>
1227   <property name="skip_pager_hint">False</property>
1228   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1229   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1230   <property name="has_separator">True</property>
1231
1232   <child internal-child="vbox">
1233     <widget class="GtkVBox" id="dialog-vbox2">
1234       <property name="visible">True</property>
1235       <property name="homogeneous">False</property>
1236       <property name="spacing">0</property>
1237
1238       <child internal-child="action_area">
1239         <widget class="GtkHButtonBox" id="dialog-action_area2">
1240           <property name="visible">True</property>
1241           <property name="layout_style">GTK_BUTTONBOX_END</property>
1242
1243           <child>
1244             <widget class="GtkButton" id="AboutDismissButton">
1245               <property name="visible">True</property>
1246               <property name="can_default">True</property>
1247               <property name="can_focus">True</property>
1248               <property name="label">gtk-ok</property>
1249               <property name="use_stock">True</property>
1250               <property name="relief">GTK_RELIEF_NORMAL</property>
1251               <property name="focus_on_click">True</property>
1252               <property name="response_id">-5</property>
1253             </widget>
1254           </child>
1255         </widget>
1256         <packing>
1257           <property name="padding">0</property>
1258           <property name="expand">False</property>
1259           <property name="fill">True</property>
1260           <property name="pack_type">GTK_PACK_END</property>
1261         </packing>
1262       </child>
1263
1264       <child>
1265         <widget class="GtkLabel" id="AboutLabel">
1266           <property name="visible">True</property>
1267           <property name="label" translatable="yes">&lt;b&gt;Matita @VERSION@&lt;/b&gt;
1268
1269 &lt;tt&gt;http://helm.cs.unibo.it&lt;/tt&gt;
1270
1271 Copyright (C) 2004,
1272 &lt;i&gt;the HELM team&lt;/i&gt;</property>
1273           <property name="use_underline">False</property>
1274           <property name="use_markup">True</property>
1275           <property name="justify">GTK_JUSTIFY_CENTER</property>
1276           <property name="wrap">False</property>
1277           <property name="selectable">False</property>
1278           <property name="xalign">0.5</property>
1279           <property name="yalign">0.5</property>
1280           <property name="xpad">5</property>
1281           <property name="ypad">5</property>
1282         </widget>
1283         <packing>
1284           <property name="padding">0</property>
1285           <property name="expand">False</property>
1286           <property name="fill">False</property>
1287         </packing>
1288       </child>
1289     </widget>
1290   </child>
1291 </widget>
1292
1293 <widget class="GtkDialog" id="UriChoiceDialog">
1294   <property name="height_request">280</property>
1295   <property name="title" translatable="yes">Uri choice</property>
1296   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1297   <property name="window_position">GTK_WIN_POS_CENTER</property>
1298   <property name="modal">True</property>
1299   <property name="resizable">True</property>
1300   <property name="destroy_with_parent">False</property>
1301   <property name="decorated">True</property>
1302   <property name="skip_taskbar_hint">False</property>
1303   <property name="skip_pager_hint">False</property>
1304   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1305   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1306   <property name="has_separator">True</property>
1307
1308   <child internal-child="vbox">
1309     <widget class="GtkVBox" id="dialog-vbox3">
1310       <property name="visible">True</property>
1311       <property name="homogeneous">False</property>
1312       <property name="spacing">0</property>
1313
1314       <child internal-child="action_area">
1315         <widget class="GtkHButtonBox" id="dialog-action_area3">
1316           <property name="visible">True</property>
1317           <property name="layout_style">GTK_BUTTONBOX_END</property>
1318
1319           <child>
1320             <widget class="GtkButton" id="UriChoiceAbortButton">
1321               <property name="visible">True</property>
1322               <property name="can_default">True</property>
1323               <property name="can_focus">True</property>
1324               <property name="label">gtk-cancel</property>
1325               <property name="use_stock">True</property>
1326               <property name="relief">GTK_RELIEF_NORMAL</property>
1327               <property name="focus_on_click">True</property>
1328               <property name="response_id">-6</property>
1329             </widget>
1330           </child>
1331
1332           <child>
1333             <widget class="GtkButton" id="UriChoiceSelectedButton">
1334               <property name="visible">True</property>
1335               <property name="can_default">True</property>
1336               <property name="can_focus">True</property>
1337               <property name="relief">GTK_RELIEF_NORMAL</property>
1338               <property name="focus_on_click">True</property>
1339               <property name="response_id">0</property>
1340
1341               <child>
1342                 <widget class="GtkAlignment" id="alignment2">
1343                   <property name="visible">True</property>
1344                   <property name="xalign">0.5</property>
1345                   <property name="yalign">0.5</property>
1346                   <property name="xscale">0</property>
1347                   <property name="yscale">0</property>
1348                   <property name="top_padding">0</property>
1349                   <property name="bottom_padding">0</property>
1350                   <property name="left_padding">0</property>
1351                   <property name="right_padding">0</property>
1352
1353                   <child>
1354                     <widget class="GtkHBox" id="hbox3">
1355                       <property name="visible">True</property>
1356                       <property name="homogeneous">False</property>
1357                       <property name="spacing">2</property>
1358
1359                       <child>
1360                         <widget class="GtkImage" id="image19">
1361                           <property name="visible">True</property>
1362                           <property name="stock">gtk-index</property>
1363                           <property name="icon_size">4</property>
1364                           <property name="xalign">0.5</property>
1365                           <property name="yalign">0.5</property>
1366                           <property name="xpad">0</property>
1367                           <property name="ypad">0</property>
1368                         </widget>
1369                         <packing>
1370                           <property name="padding">0</property>
1371                           <property name="expand">False</property>
1372                           <property name="fill">False</property>
1373                         </packing>
1374                       </child>
1375
1376                       <child>
1377                         <widget class="GtkLabel" id="label3">
1378                           <property name="visible">True</property>
1379                           <property name="label" translatable="yes">Try _Selected</property>
1380                           <property name="use_underline">True</property>
1381                           <property name="use_markup">False</property>
1382                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1383                           <property name="wrap">False</property>
1384                           <property name="selectable">False</property>
1385                           <property name="xalign">0.5</property>
1386                           <property name="yalign">0.5</property>
1387                           <property name="xpad">0</property>
1388                           <property name="ypad">0</property>
1389                         </widget>
1390                         <packing>
1391                           <property name="padding">0</property>
1392                           <property name="expand">False</property>
1393                           <property name="fill">False</property>
1394                         </packing>
1395                       </child>
1396                     </widget>
1397                   </child>
1398                 </widget>
1399               </child>
1400             </widget>
1401           </child>
1402
1403           <child>
1404             <widget class="GtkButton" id="UriChoiceConstantsButton">
1405               <property name="visible">True</property>
1406               <property name="sensitive">False</property>
1407               <property name="can_default">True</property>
1408               <property name="can_focus">True</property>
1409               <property name="label" translatable="yes">Try Constants</property>
1410               <property name="use_underline">True</property>
1411               <property name="relief">GTK_RELIEF_NORMAL</property>
1412               <property name="focus_on_click">True</property>
1413               <property name="response_id">0</property>
1414             </widget>
1415           </child>
1416
1417           <child>
1418             <widget class="GtkButton" id="UriChoiceAutoButton">
1419               <property name="visible">True</property>
1420               <property name="can_default">True</property>
1421               <property name="can_focus">True</property>
1422               <property name="relief">GTK_RELIEF_NORMAL</property>
1423               <property name="focus_on_click">True</property>
1424               <property name="response_id">0</property>
1425
1426               <child>
1427                 <widget class="GtkAlignment" id="alignment1">
1428                   <property name="visible">True</property>
1429                   <property name="xalign">0.5</property>
1430                   <property name="yalign">0.5</property>
1431                   <property name="xscale">0</property>
1432                   <property name="yscale">0</property>
1433                   <property name="top_padding">0</property>
1434                   <property name="bottom_padding">0</property>
1435                   <property name="left_padding">0</property>
1436                   <property name="right_padding">0</property>
1437
1438                   <child>
1439                     <widget class="GtkHBox" id="hbox1">
1440                       <property name="visible">True</property>
1441                       <property name="homogeneous">False</property>
1442                       <property name="spacing">2</property>
1443
1444                       <child>
1445                         <widget class="GtkImage" id="image18">
1446                           <property name="visible">True</property>
1447                           <property name="stock">gtk-ok</property>
1448                           <property name="icon_size">4</property>
1449                           <property name="xalign">0.5</property>
1450                           <property name="yalign">0.5</property>
1451                           <property name="xpad">0</property>
1452                           <property name="ypad">0</property>
1453                         </widget>
1454                         <packing>
1455                           <property name="padding">0</property>
1456                           <property name="expand">False</property>
1457                           <property name="fill">False</property>
1458                         </packing>
1459                       </child>
1460
1461                       <child>
1462                         <widget class="GtkLabel" id="label1">
1463                           <property name="visible">True</property>
1464                           <property name="label" translatable="yes">_Auto</property>
1465                           <property name="use_underline">True</property>
1466                           <property name="use_markup">False</property>
1467                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1468                           <property name="wrap">False</property>
1469                           <property name="selectable">False</property>
1470                           <property name="xalign">0.5</property>
1471                           <property name="yalign">0.5</property>
1472                           <property name="xpad">0</property>
1473                           <property name="ypad">0</property>
1474                         </widget>
1475                         <packing>
1476                           <property name="padding">0</property>
1477                           <property name="expand">False</property>
1478                           <property name="fill">False</property>
1479                         </packing>
1480                       </child>
1481                     </widget>
1482                   </child>
1483                 </widget>
1484               </child>
1485             </widget>
1486           </child>
1487         </widget>
1488         <packing>
1489           <property name="padding">0</property>
1490           <property name="expand">False</property>
1491           <property name="fill">True</property>
1492           <property name="pack_type">GTK_PACK_END</property>
1493         </packing>
1494       </child>
1495
1496       <child>
1497         <widget class="GtkVBox" id="vbox2">
1498           <property name="visible">True</property>
1499           <property name="homogeneous">False</property>
1500           <property name="spacing">0</property>
1501
1502           <child>
1503             <widget class="GtkLabel" id="UriChoiceLabel">
1504               <property name="visible">True</property>
1505               <property name="label" translatable="yes">some informative message here ...</property>
1506               <property name="use_underline">False</property>
1507               <property name="use_markup">False</property>
1508               <property name="justify">GTK_JUSTIFY_LEFT</property>
1509               <property name="wrap">False</property>
1510               <property name="selectable">False</property>
1511               <property name="xalign">0.5</property>
1512               <property name="yalign">0.5</property>
1513               <property name="xpad">0</property>
1514               <property name="ypad">0</property>
1515             </widget>
1516             <packing>
1517               <property name="padding">0</property>
1518               <property name="expand">False</property>
1519               <property name="fill">False</property>
1520             </packing>
1521           </child>
1522
1523           <child>
1524             <widget class="GtkScrolledWindow" id="scrolledwindow1">
1525               <property name="visible">True</property>
1526               <property name="can_focus">True</property>
1527               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1528               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1529               <property name="shadow_type">GTK_SHADOW_NONE</property>
1530               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1531
1532               <child>
1533                 <widget class="GtkTreeView" id="UriChoiceTreeView">
1534                   <property name="visible">True</property>
1535                   <property name="can_focus">True</property>
1536                   <property name="headers_visible">False</property>
1537                   <property name="rules_hint">False</property>
1538                   <property name="reorderable">False</property>
1539                   <property name="enable_search">True</property>
1540                 </widget>
1541               </child>
1542             </widget>
1543             <packing>
1544               <property name="padding">0</property>
1545               <property name="expand">True</property>
1546               <property name="fill">True</property>
1547             </packing>
1548           </child>
1549
1550           <child>
1551             <widget class="GtkHBox" id="hbox2">
1552               <property name="visible">True</property>
1553               <property name="homogeneous">False</property>
1554               <property name="spacing">0</property>
1555
1556               <child>
1557                 <widget class="GtkLabel" id="label2">
1558                   <property name="visible">True</property>
1559                   <property name="label" translatable="yes">URI: </property>
1560                   <property name="use_underline">False</property>
1561                   <property name="use_markup">False</property>
1562                   <property name="justify">GTK_JUSTIFY_LEFT</property>
1563                   <property name="wrap">False</property>
1564                   <property name="selectable">False</property>
1565                   <property name="xalign">0.5</property>
1566                   <property name="yalign">0.5</property>
1567                   <property name="xpad">0</property>
1568                   <property name="ypad">0</property>
1569                 </widget>
1570                 <packing>
1571                   <property name="padding">0</property>
1572                   <property name="expand">False</property>
1573                   <property name="fill">False</property>
1574                 </packing>
1575               </child>
1576
1577               <child>
1578                 <widget class="GtkEntry" id="entry1">
1579                   <property name="visible">True</property>
1580                   <property name="can_focus">True</property>
1581                   <property name="editable">True</property>
1582                   <property name="visibility">True</property>
1583                   <property name="max_length">0</property>
1584                   <property name="text" translatable="yes"></property>
1585                   <property name="has_frame">True</property>
1586                   <property name="invisible_char">*</property>
1587                   <property name="activates_default">False</property>
1588                 </widget>
1589                 <packing>
1590                   <property name="padding">0</property>
1591                   <property name="expand">True</property>
1592                   <property name="fill">True</property>
1593                 </packing>
1594               </child>
1595             </widget>
1596             <packing>
1597               <property name="padding">0</property>
1598               <property name="expand">False</property>
1599               <property name="fill">True</property>
1600             </packing>
1601           </child>
1602         </widget>
1603         <packing>
1604           <property name="padding">0</property>
1605           <property name="expand">True</property>
1606           <property name="fill">True</property>
1607         </packing>
1608       </child>
1609     </widget>
1610   </child>
1611 </widget>
1612
1613 <widget class="GtkDialog" id="InterpChoiceDialog">
1614   <property name="height_request">200</property>
1615   <property name="title" translatable="yes">Interpretation choice</property>
1616   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1617   <property name="window_position">GTK_WIN_POS_NONE</property>
1618   <property name="modal">True</property>
1619   <property name="resizable">True</property>
1620   <property name="destroy_with_parent">False</property>
1621   <property name="decorated">True</property>
1622   <property name="skip_taskbar_hint">False</property>
1623   <property name="skip_pager_hint">False</property>
1624   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1625   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1626   <property name="has_separator">True</property>
1627
1628   <child internal-child="vbox">
1629     <widget class="GtkVBox" id="dialog-vbox4">
1630       <property name="visible">True</property>
1631       <property name="homogeneous">False</property>
1632       <property name="spacing">0</property>
1633
1634       <child internal-child="action_area">
1635         <widget class="GtkHButtonBox" id="dialog-action_area4">
1636           <property name="visible">True</property>
1637           <property name="layout_style">GTK_BUTTONBOX_END</property>
1638
1639           <child>
1640             <widget class="GtkButton" id="InterpChoiceHelpButton">
1641               <property name="visible">True</property>
1642               <property name="can_default">True</property>
1643               <property name="can_focus">True</property>
1644               <property name="label">gtk-help</property>
1645               <property name="use_stock">True</property>
1646               <property name="relief">GTK_RELIEF_NORMAL</property>
1647               <property name="focus_on_click">True</property>
1648               <property name="response_id">-11</property>
1649             </widget>
1650           </child>
1651
1652           <child>
1653             <widget class="GtkButton" id="InterpChoiceCancelButton">
1654               <property name="visible">True</property>
1655               <property name="can_default">True</property>
1656               <property name="can_focus">True</property>
1657               <property name="label">gtk-cancel</property>
1658               <property name="use_stock">True</property>
1659               <property name="relief">GTK_RELIEF_NORMAL</property>
1660               <property name="focus_on_click">True</property>
1661               <property name="response_id">-6</property>
1662             </widget>
1663           </child>
1664
1665           <child>
1666             <widget class="GtkButton" id="InterpChoiceOkButton">
1667               <property name="visible">True</property>
1668               <property name="can_default">True</property>
1669               <property name="can_focus">True</property>
1670               <property name="label">gtk-ok</property>
1671               <property name="use_stock">True</property>
1672               <property name="relief">GTK_RELIEF_NORMAL</property>
1673               <property name="focus_on_click">True</property>
1674               <property name="response_id">-5</property>
1675             </widget>
1676           </child>
1677         </widget>
1678         <packing>
1679           <property name="padding">0</property>
1680           <property name="expand">False</property>
1681           <property name="fill">True</property>
1682           <property name="pack_type">GTK_PACK_END</property>
1683         </packing>
1684       </child>
1685
1686       <child>
1687         <widget class="GtkVBox" id="vbox3">
1688           <property name="visible">True</property>
1689           <property name="homogeneous">False</property>
1690           <property name="spacing">0</property>
1691
1692           <child>
1693             <widget class="GtkLabel" id="InterpChoiceDialogLabel">
1694               <property name="visible">True</property>
1695               <property name="label" translatable="yes">some informative message here ...</property>
1696               <property name="use_underline">False</property>
1697               <property name="use_markup">False</property>
1698               <property name="justify">GTK_JUSTIFY_LEFT</property>
1699               <property name="wrap">False</property>
1700               <property name="selectable">False</property>
1701               <property name="xalign">0.5</property>
1702               <property name="yalign">0.5</property>
1703               <property name="xpad">0</property>
1704               <property name="ypad">0</property>
1705             </widget>
1706             <packing>
1707               <property name="padding">0</property>
1708               <property name="expand">False</property>
1709               <property name="fill">False</property>
1710             </packing>
1711           </child>
1712
1713           <child>
1714             <widget class="GtkScrolledWindow" id="scrolledwindow4">
1715               <property name="visible">True</property>
1716               <property name="can_focus">True</property>
1717               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1718               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1719               <property name="shadow_type">GTK_SHADOW_IN</property>
1720               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1721
1722               <child>
1723                 <widget class="GtkTreeView" id="InterpChoiceTreeView">
1724                   <property name="visible">True</property>
1725                   <property name="can_focus">True</property>
1726                   <property name="headers_visible">False</property>
1727                   <property name="rules_hint">False</property>
1728                   <property name="reorderable">False</property>
1729                   <property name="enable_search">True</property>
1730                 </widget>
1731               </child>
1732             </widget>
1733             <packing>
1734               <property name="padding">0</property>
1735               <property name="expand">True</property>
1736               <property name="fill">True</property>
1737             </packing>
1738           </child>
1739         </widget>
1740         <packing>
1741           <property name="padding">0</property>
1742           <property name="expand">True</property>
1743           <property name="fill">True</property>
1744         </packing>
1745       </child>
1746     </widget>
1747   </child>
1748 </widget>
1749
1750 <widget class="GtkDialog" id="EmptyDialog">
1751   <property name="visible">True</property>
1752   <property name="title" translatable="yes">DUMMY</property>
1753   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1754   <property name="window_position">GTK_WIN_POS_NONE</property>
1755   <property name="modal">False</property>
1756   <property name="resizable">True</property>
1757   <property name="destroy_with_parent">False</property>
1758   <property name="decorated">True</property>
1759   <property name="skip_taskbar_hint">False</property>
1760   <property name="skip_pager_hint">False</property>
1761   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1762   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1763   <property name="has_separator">True</property>
1764
1765   <child internal-child="vbox">
1766     <widget class="GtkVBox" id="EmptyDialogVBox">
1767       <property name="visible">True</property>
1768       <property name="homogeneous">False</property>
1769       <property name="spacing">0</property>
1770
1771       <child internal-child="action_area">
1772         <widget class="GtkHButtonBox" id="dialog-action_area5">
1773           <property name="visible">True</property>
1774           <property name="layout_style">GTK_BUTTONBOX_END</property>
1775
1776           <child>
1777             <widget class="GtkButton" id="EmptyDialogCancelButton">
1778               <property name="visible">True</property>
1779               <property name="can_default">True</property>
1780               <property name="can_focus">True</property>
1781               <property name="label">gtk-cancel</property>
1782               <property name="use_stock">True</property>
1783               <property name="relief">GTK_RELIEF_NORMAL</property>
1784               <property name="focus_on_click">True</property>
1785               <property name="response_id">-6</property>
1786             </widget>
1787           </child>
1788
1789           <child>
1790             <widget class="GtkButton" id="EmptyDialogOkButton">
1791               <property name="visible">True</property>
1792               <property name="can_default">True</property>
1793               <property name="can_focus">True</property>
1794               <property name="label">gtk-ok</property>
1795               <property name="use_stock">True</property>
1796               <property name="relief">GTK_RELIEF_NORMAL</property>
1797               <property name="focus_on_click">True</property>
1798               <property name="response_id">-5</property>
1799             </widget>
1800           </child>
1801         </widget>
1802         <packing>
1803           <property name="padding">0</property>
1804           <property name="expand">False</property>
1805           <property name="fill">True</property>
1806           <property name="pack_type">GTK_PACK_END</property>
1807         </packing>
1808       </child>
1809
1810       <child>
1811         <widget class="GtkLabel" id="EmptyDialogLabel">
1812           <property name="visible">True</property>
1813           <property name="label" translatable="yes">DUMMY</property>
1814           <property name="use_underline">False</property>
1815           <property name="use_markup">False</property>
1816           <property name="justify">GTK_JUSTIFY_LEFT</property>
1817           <property name="wrap">False</property>
1818           <property name="selectable">False</property>
1819           <property name="xalign">0.5</property>
1820           <property name="yalign">0.5</property>
1821           <property name="xpad">0</property>
1822           <property name="ypad">0</property>
1823         </widget>
1824         <packing>
1825           <property name="padding">0</property>
1826           <property name="expand">False</property>
1827           <property name="fill">False</property>
1828         </packing>
1829       </child>
1830
1831       <child>
1832         <placeholder/>
1833       </child>
1834     </widget>
1835   </child>
1836 </widget>
1837
1838 <widget class="GtkWindow" id="CheckWin">
1839   <property name="width_request">300</property>
1840   <property name="height_request">200</property>
1841   <property name="title" translatable="yes">Matita: check term</property>
1842   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1843   <property name="window_position">GTK_WIN_POS_NONE</property>
1844   <property name="modal">False</property>
1845   <property name="resizable">True</property>
1846   <property name="destroy_with_parent">False</property>
1847   <property name="decorated">True</property>
1848   <property name="skip_taskbar_hint">False</property>
1849   <property name="skip_pager_hint">False</property>
1850   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1851   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1852
1853   <child>
1854     <widget class="GtkEventBox" id="CheckWinEventBox">
1855       <property name="visible">True</property>
1856       <property name="visible_window">True</property>
1857       <property name="above_child">False</property>
1858
1859       <child>
1860         <widget class="GtkScrolledWindow" id="ScrolledCheck">
1861           <property name="visible">True</property>
1862           <property name="can_focus">True</property>
1863           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1864           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1865           <property name="shadow_type">GTK_SHADOW_IN</property>
1866           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1867
1868           <child>
1869             <placeholder/>
1870           </child>
1871         </widget>
1872       </child>
1873     </widget>
1874   </child>
1875 </widget>
1876
1877 <widget class="GtkWindow" id="ScriptWin">
1878   <property name="title" translatable="yes">Matita: script</property>
1879   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1880   <property name="window_position">GTK_WIN_POS_NONE</property>
1881   <property name="modal">False</property>
1882   <property name="default_width">450</property>
1883   <property name="default_height">800</property>
1884   <property name="resizable">True</property>
1885   <property name="destroy_with_parent">False</property>
1886   <property name="decorated">True</property>
1887   <property name="skip_taskbar_hint">False</property>
1888   <property name="skip_pager_hint">False</property>
1889   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1890   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1891
1892   <child>
1893     <widget class="GtkEventBox" id="ScriptWinEventBox">
1894       <property name="visible">True</property>
1895       <property name="visible_window">True</property>
1896       <property name="above_child">False</property>
1897
1898       <child>
1899         <widget class="GtkNotebook" id="scriptNotebook">
1900           <property name="visible">True</property>
1901           <property name="can_focus">True</property>
1902           <property name="show_tabs">True</property>
1903           <property name="show_border">True</property>
1904           <property name="tab_pos">GTK_POS_BOTTOM</property>
1905           <property name="scrollable">False</property>
1906           <property name="enable_popup">False</property>
1907
1908           <child>
1909             <widget class="GtkVBox" id="vbox4">
1910               <property name="visible">True</property>
1911               <property name="homogeneous">False</property>
1912               <property name="spacing">0</property>
1913
1914               <child>
1915                 <widget class="GtkToolbar" id="toolbar1">
1916                   <property name="visible">True</property>
1917                   <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1918                   <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1919                   <property name="tooltips">True</property>
1920                   <property name="show_arrow">True</property>
1921
1922                   <child>
1923                     <widget class="GtkToolItem" id="toolitem1">
1924                       <property name="visible">True</property>
1925                       <property name="visible_horizontal">True</property>
1926                       <property name="visible_vertical">True</property>
1927                       <property name="is_important">False</property>
1928
1929                       <child>
1930                         <widget class="GtkButton" id="ScriptWinBackButton">
1931                           <property name="visible">True</property>
1932                           <property name="tooltip" translatable="yes">go back 1 phrase</property>
1933                           <property name="can_focus">True</property>
1934                           <property name="relief">GTK_RELIEF_NORMAL</property>
1935                           <property name="focus_on_click">True</property>
1936
1937                           <child>
1938                             <widget class="GtkImage" id="image133">
1939                               <property name="visible">True</property>
1940                               <property name="stock">gtk-go-back</property>
1941                               <property name="icon_size">4</property>
1942                               <property name="xalign">0.5</property>
1943                               <property name="yalign">0.5</property>
1944                               <property name="xpad">0</property>
1945                               <property name="ypad">0</property>
1946                             </widget>
1947                           </child>
1948                         </widget>
1949                       </child>
1950                     </widget>
1951                     <packing>
1952                       <property name="expand">False</property>
1953                       <property name="homogeneous">False</property>
1954                     </packing>
1955                   </child>
1956
1957                   <child>
1958                     <widget class="GtkToolItem" id="toolitem2">
1959                       <property name="visible">True</property>
1960                       <property name="visible_horizontal">True</property>
1961                       <property name="visible_vertical">True</property>
1962                       <property name="is_important">False</property>
1963
1964                       <child>
1965                         <widget class="GtkButton" id="ScriptWinJumpButton">
1966                           <property name="visible">True</property>
1967                           <property name="tooltip" translatable="yes">execute til cursor</property>
1968                           <property name="can_focus">True</property>
1969                           <property name="relief">GTK_RELIEF_NORMAL</property>
1970                           <property name="focus_on_click">True</property>
1971
1972                           <child>
1973                             <widget class="GtkImage" id="image134">
1974                               <property name="visible">True</property>
1975                               <property name="stock">gtk-jump-to</property>
1976                               <property name="icon_size">4</property>
1977                               <property name="xalign">0.5</property>
1978                               <property name="yalign">0.5</property>
1979                               <property name="xpad">0</property>
1980                               <property name="ypad">0</property>
1981                             </widget>
1982                           </child>
1983                         </widget>
1984                       </child>
1985                     </widget>
1986                     <packing>
1987                       <property name="expand">False</property>
1988                       <property name="homogeneous">False</property>
1989                     </packing>
1990                   </child>
1991
1992                   <child>
1993                     <widget class="GtkToolItem" id="toolitem3">
1994                       <property name="visible">True</property>
1995                       <property name="visible_horizontal">True</property>
1996                       <property name="visible_vertical">True</property>
1997                       <property name="is_important">False</property>
1998
1999                       <child>
2000                         <widget class="GtkButton" id="ScriptWinForwardButton">
2001                           <property name="visible">True</property>
2002                           <property name="tooltip" translatable="yes">go forward 1 phrase</property>
2003                           <property name="can_focus">True</property>
2004                           <property name="relief">GTK_RELIEF_NORMAL</property>
2005                           <property name="focus_on_click">True</property>
2006
2007                           <child>
2008                             <widget class="GtkImage" id="image135">
2009                               <property name="visible">True</property>
2010                               <property name="stock">gtk-go-forward</property>
2011                               <property name="icon_size">4</property>
2012                               <property name="xalign">0.5</property>
2013                               <property name="yalign">0.5</property>
2014                               <property name="xpad">0</property>
2015                               <property name="ypad">0</property>
2016                             </widget>
2017                           </child>
2018                         </widget>
2019                       </child>
2020                     </widget>
2021                     <packing>
2022                       <property name="expand">False</property>
2023                       <property name="homogeneous">False</property>
2024                     </packing>
2025                   </child>
2026                 </widget>
2027                 <packing>
2028                   <property name="padding">0</property>
2029                   <property name="expand">False</property>
2030                   <property name="fill">False</property>
2031                 </packing>
2032               </child>
2033
2034               <child>
2035                 <widget class="GtkScrolledWindow" id="ScrolledScript">
2036                   <property name="visible">True</property>
2037                   <property name="can_focus">True</property>
2038                   <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
2039                   <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2040                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2041                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2042
2043                   <child>
2044                     <widget class="GtkTextView" id="ScriptTextView">
2045                       <property name="visible">True</property>
2046                       <property name="can_focus">True</property>
2047                       <property name="editable">True</property>
2048                       <property name="overwrite">False</property>
2049                       <property name="accepts_tab">True</property>
2050                       <property name="justification">GTK_JUSTIFY_LEFT</property>
2051                       <property name="wrap_mode">GTK_WRAP_NONE</property>
2052                       <property name="cursor_visible">True</property>
2053                       <property name="pixels_above_lines">0</property>
2054                       <property name="pixels_below_lines">0</property>
2055                       <property name="pixels_inside_wrap">0</property>
2056                       <property name="left_margin">0</property>
2057                       <property name="right_margin">0</property>
2058                       <property name="indent">0</property>
2059                       <property name="text" translatable="yes"></property>
2060                     </widget>
2061                   </child>
2062                 </widget>
2063                 <packing>
2064                   <property name="padding">0</property>
2065                   <property name="expand">True</property>
2066                   <property name="fill">True</property>
2067                 </packing>
2068               </child>
2069             </widget>
2070             <packing>
2071               <property name="tab_expand">False</property>
2072               <property name="tab_fill">True</property>
2073             </packing>
2074           </child>
2075
2076           <child>
2077             <widget class="GtkLabel" id="label7">
2078               <property name="visible">True</property>
2079               <property name="label" translatable="yes">script</property>
2080               <property name="use_underline">False</property>
2081               <property name="use_markup">False</property>
2082               <property name="justify">GTK_JUSTIFY_LEFT</property>
2083               <property name="wrap">False</property>
2084               <property name="selectable">False</property>
2085               <property name="xalign">0.5</property>
2086               <property name="yalign">0.5</property>
2087               <property name="xpad">0</property>
2088               <property name="ypad">0</property>
2089             </widget>
2090             <packing>
2091               <property name="type">tab</property>
2092             </packing>
2093           </child>
2094
2095           <child>
2096             <widget class="GtkScrolledWindow" id="scrolledwindow3">
2097               <property name="visible">True</property>
2098               <property name="can_focus">True</property>
2099               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
2100               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2101               <property name="shadow_type">GTK_SHADOW_IN</property>
2102               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2103
2104               <child>
2105                 <widget class="GtkTreeView" id="treeview1">
2106                   <property name="visible">True</property>
2107                   <property name="can_focus">True</property>
2108                   <property name="headers_visible">False</property>
2109                   <property name="rules_hint">False</property>
2110                   <property name="reorderable">False</property>
2111                   <property name="enable_search">True</property>
2112                 </widget>
2113               </child>
2114             </widget>
2115             <packing>
2116               <property name="tab_expand">False</property>
2117               <property name="tab_fill">True</property>
2118             </packing>
2119           </child>
2120
2121           <child>
2122             <widget class="GtkLabel" id="label8">
2123               <property name="visible">True</property>
2124               <property name="label" translatable="yes">outline</property>
2125               <property name="use_underline">False</property>
2126               <property name="use_markup">False</property>
2127               <property name="justify">GTK_JUSTIFY_LEFT</property>
2128               <property name="wrap">False</property>
2129               <property name="selectable">False</property>
2130               <property name="xalign">0.5</property>
2131               <property name="yalign">0.5</property>
2132               <property name="xpad">0</property>
2133               <property name="ypad">0</property>
2134             </widget>
2135             <packing>
2136               <property name="type">tab</property>
2137             </packing>
2138           </child>
2139         </widget>
2140       </child>
2141     </widget>
2142   </child>
2143 </widget>
2144
2145 <widget class="GtkDialog" id="TextDialog">
2146   <property name="title" translatable="yes">DUMMY</property>
2147   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2148   <property name="window_position">GTK_WIN_POS_NONE</property>
2149   <property name="modal">False</property>
2150   <property name="resizable">True</property>
2151   <property name="destroy_with_parent">False</property>
2152   <property name="decorated">True</property>
2153   <property name="skip_taskbar_hint">False</property>
2154   <property name="skip_pager_hint">False</property>
2155   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2156   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2157   <property name="has_separator">True</property>
2158
2159   <child internal-child="vbox">
2160     <widget class="GtkVBox" id="vbox5">
2161       <property name="visible">True</property>
2162       <property name="homogeneous">False</property>
2163       <property name="spacing">0</property>
2164
2165       <child internal-child="action_area">
2166         <widget class="GtkHButtonBox" id="hbuttonbox1">
2167           <property name="visible">True</property>
2168           <property name="layout_style">GTK_BUTTONBOX_END</property>
2169
2170           <child>
2171             <widget class="GtkButton" id="TextDialogCancelButton">
2172               <property name="visible">True</property>
2173               <property name="can_default">True</property>
2174               <property name="can_focus">True</property>
2175               <property name="label">gtk-cancel</property>
2176               <property name="use_stock">True</property>
2177               <property name="relief">GTK_RELIEF_NORMAL</property>
2178               <property name="focus_on_click">True</property>
2179               <property name="response_id">-6</property>
2180             </widget>
2181           </child>
2182
2183           <child>
2184             <widget class="GtkButton" id="TextDialogOkButton">
2185               <property name="visible">True</property>
2186               <property name="can_default">True</property>
2187               <property name="can_focus">True</property>
2188               <property name="label">gtk-ok</property>
2189               <property name="use_stock">True</property>
2190               <property name="relief">GTK_RELIEF_NORMAL</property>
2191               <property name="focus_on_click">True</property>
2192               <property name="response_id">-5</property>
2193             </widget>
2194           </child>
2195         </widget>
2196         <packing>
2197           <property name="padding">0</property>
2198           <property name="expand">False</property>
2199           <property name="fill">True</property>
2200           <property name="pack_type">GTK_PACK_END</property>
2201         </packing>
2202       </child>
2203
2204       <child>
2205         <widget class="GtkLabel" id="TextDialogLabel">
2206           <property name="visible">True</property>
2207           <property name="label" translatable="yes">DUMMY</property>
2208           <property name="use_underline">False</property>
2209           <property name="use_markup">False</property>
2210           <property name="justify">GTK_JUSTIFY_LEFT</property>
2211           <property name="wrap">False</property>
2212           <property name="selectable">False</property>
2213           <property name="xalign">0.5</property>
2214           <property name="yalign">0.5</property>
2215           <property name="xpad">0</property>
2216           <property name="ypad">0</property>
2217         </widget>
2218         <packing>
2219           <property name="padding">0</property>
2220           <property name="expand">False</property>
2221           <property name="fill">False</property>
2222         </packing>
2223       </child>
2224
2225       <child>
2226         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2227           <property name="visible">True</property>
2228           <property name="can_focus">True</property>
2229           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2230           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2231           <property name="shadow_type">GTK_SHADOW_IN</property>
2232           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2233
2234           <child>
2235             <widget class="GtkTextView" id="TextDialogTextView">
2236               <property name="visible">True</property>
2237               <property name="can_focus">True</property>
2238               <property name="editable">True</property>
2239               <property name="overwrite">False</property>
2240               <property name="accepts_tab">True</property>
2241               <property name="justification">GTK_JUSTIFY_LEFT</property>
2242               <property name="wrap_mode">GTK_WRAP_NONE</property>
2243               <property name="cursor_visible">True</property>
2244               <property name="pixels_above_lines">0</property>
2245               <property name="pixels_below_lines">0</property>
2246               <property name="pixels_inside_wrap">0</property>
2247               <property name="left_margin">0</property>
2248               <property name="right_margin">0</property>
2249               <property name="indent">0</property>
2250               <property name="text" translatable="yes"></property>
2251             </widget>
2252           </child>
2253         </widget>
2254         <packing>
2255           <property name="padding">0</property>
2256           <property name="expand">True</property>
2257           <property name="fill">True</property>
2258         </packing>
2259       </child>
2260     </widget>
2261   </child>
2262 </widget>
2263
2264 </glade-interface>