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="image128">
  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                                 </widget>
  74                               </child>
  75
  76                               <child>
  77                                 <widget class="GtkMenuItem" id="NewDefsMenuItem">
  78                                   <property name="visible">True</property>
  79                                   <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
  80                                   <property name="use_underline">True</property>
  81                                 </widget>
  82                               </child>
  83                             </widget>
  84                           </child>
  85                         </widget>
  86                       </child>
  87
  88                       <child>
  89                         <widget class="GtkImageMenuItem" id="OpenMenuItem">
  90                           <property name="visible">True</property>
  91                           <property name="label" translatable="yes">_Open...</property>
  92                           <property name="use_underline">True</property>
  93                           <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
  94
  95                           <child internal-child="image">
  96                             <widget class="GtkImage" id="image129">
  97                               <property name="visible">True</property>
  98                               <property name="stock">gtk-open</property>
  99                               <property name="icon_size">1</property>
 100                               <property name="xalign">0.5</property>
 101                               <property name="yalign">0.5</property>
 102                               <property name="xpad">0</property>
 103                               <property name="ypad">0</property>
 104                             </widget>
 105                           </child>
 106                         </widget>
 107                       </child>
 108
 109                       <child>
 110                         <widget class="GtkImageMenuItem" id="SaveMenuItem">
 111                           <property name="visible">True</property>
 112                           <property name="label" translatable="yes">_Save</property>
 113                           <property name="use_underline">True</property>
 114                           <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 115
 116                           <child internal-child="image">
 117                             <widget class="GtkImage" id="image130">
 118                               <property name="visible">True</property>
 119                               <property name="stock">gtk-save</property>
 120                               <property name="icon_size">1</property>
 121                               <property name="xalign">0.5</property>
 122                               <property name="yalign">0.5</property>
 123                               <property name="xpad">0</property>
 124                               <property name="ypad">0</property>
 125                             </widget>
 126                           </child>
 127                         </widget>
 128                       </child>
 129
 130                       <child>
 131                         <widget class="GtkImageMenuItem" id="SaveAsMenuItem">
 132                           <property name="visible">True</property>
 133                           <property name="label" translatable="yes">Save _As ...</property>
 134                           <property name="use_underline">True</property>
 135
 136                           <child internal-child="image">
 137                             <widget class="GtkImage" id="image131">
 138                               <property name="visible">True</property>
 139                               <property name="stock">gtk-save-as</property>
 140                               <property name="icon_size">1</property>
 141                               <property name="xalign">0.5</property>
 142                               <property name="yalign">0.5</property>
 143                               <property name="xpad">0</property>
 144                               <property name="ypad">0</property>
 145                             </widget>
 146                           </child>
 147                         </widget>
 148                       </child>
 149
 150                       <child>
 151                         <widget class="GtkSeparatorMenuItem" id="separator1">
 152                           <property name="visible">True</property>
 153                         </widget>
 154                       </child>
 155
 156                       <child>
 157                         <widget class="GtkImageMenuItem" id="QuitMenuItem">
 158                           <property name="visible">True</property>
 159                           <property name="label" translatable="yes">_Quit</property>
 160                           <property name="use_underline">True</property>
 161                           <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 162
 163                           <child internal-child="image">
 164                             <widget class="GtkImage" id="image132">
 165                               <property name="visible">True</property>
 166                               <property name="stock">gtk-quit</property>
 167                               <property name="icon_size">1</property>
 168                               <property name="xalign">0.5</property>
 169                               <property name="yalign">0.5</property>
 170                               <property name="xpad">0</property>
 171                               <property name="ypad">0</property>
 172                             </widget>
 173                           </child>
 174                         </widget>
 175                       </child>
 176                     </widget>
 177                   </child>
 178                 </widget>
 179               </child>
 180
 181               <child>
 182                 <widget class="GtkMenuItem" id="EditMenu">
 183                   <property name="visible">True</property>
 184                   <property name="label" translatable="yes">_Edit</property>
 185                   <property name="use_underline">True</property>
 186                 </widget>
 187               </child>
 188
 189               <child>
 190                 <widget class="GtkMenuItem" id="ViewMenu">
 191                   <property name="visible">True</property>
 192                   <property name="label" translatable="yes">_View</property>
 193                   <property name="use_underline">True</property>
 194
 195                   <child>
 196                     <widget class="GtkMenu" id="ViewMenu_menu">
 197
 198                       <child>
 199                         <widget class="GtkCheckMenuItem" id="ShowToolBarMenuItem">
 200                           <property name="visible">True</property>
 201                           <property name="label" translatable="yes">Show Button Bar</property>
 202                           <property name="use_underline">True</property>
 203                           <property name="active">True</property>
 204                         </widget>
 205                       </child>
 206
 207                       <child>
 208                         <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
 209                           <property name="visible">True</property>
 210                           <property name="label" translatable="yes">Show Proof Window</property>
 211                           <property name="use_underline">True</property>
 212                           <property name="active">False</property>
 213                           <accelerator key="F3" modifiers="0" signal="activate"/>
 214                         </widget>
 215                       </child>
 216
 217                       <child>
 218                         <widget class="GtkCheckMenuItem" id="ShowCheckMenuItem">
 219                           <property name="visible">True</property>
 220                           <property name="label" translatable="yes">Show Check Window</property>
 221                           <property name="use_underline">True</property>
 222                           <property name="active">False</property>
 223                           <accelerator key="F4" modifiers="0" signal="activate"/>
 224                         </widget>
 225                       </child>
 226
 227                       <child>
 228                         <widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
 229                           <property name="visible">True</property>
 230                           <property name="label" translatable="yes">Show Script Window</property>
 231                           <property name="use_underline">True</property>
 232                           <property name="active">False</property>
 233                           <accelerator key="F5" modifiers="0" signal="activate"/>
 234                         </widget>
 235                       </child>
 236                     </widget>
 237                   </child>
 238                 </widget>
 239               </child>
 240
 241               <child>
 242                 <widget class="GtkMenuItem" id="DebugMenu">
 243                   <property name="visible">True</property>
 244                   <property name="label" translatable="yes">Debug</property>
 245                   <property name="use_underline">True</property>
 246
 247                   <child>
 248                     <widget class="GtkMenu" id="DebugMenu_menu">
 249
 250                       <child>
 251                         <widget class="GtkSeparatorMenuItem" id="separator2">
 252                           <property name="visible">True</property>
 253                         </widget>
 254                       </child>
 255                     </widget>
 256                   </child>
 257                 </widget>
 258               </child>
 259
 260               <child>
 261                 <widget class="GtkMenuItem" id="HelpMenu">
 262                   <property name="visible">True</property>
 263                   <property name="label" translatable="yes">_Help</property>
 264                   <property name="use_underline">True</property>
 265
 266                   <child>
 267                     <widget class="GtkMenu" id="HelpMenu_menu">
 268
 269                       <child>
 270                         <widget class="GtkMenuItem" id="AboutMenuItem">
 271                           <property name="visible">True</property>
 272                           <property name="label" translatable="yes">About...</property>
 273                           <property name="use_underline">True</property>
 274                         </widget>
 275                       </child>
 276                     </widget>
 277                   </child>
 278                 </widget>
 279               </child>
 280             </widget>
 281             <packing>
 282               <property name="padding">0</property>
 283               <property name="expand">False</property>
 284               <property name="fill">False</property>
 285             </packing>
 286           </child>
 287
 288           <child>
 289             <widget class="GtkVPaned" id="MainVPanes">
 290               <property name="visible">True</property>
 291               <property name="can_focus">True</property>
 292               <property name="position">450</property>
 293
 294               <child>
 295                 <widget class="GtkScrolledWindow" id="ScrolledSequents">
 296                   <property name="visible">True</property>
 297                   <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
 298                   <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
 299                   <property name="shadow_type">GTK_SHADOW_NONE</property>
 300                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 301
 302                   <child>
 303                     <widget class="GtkViewport" id="viewport1">
 304                       <property name="visible">True</property>
 305                       <property name="shadow_type">GTK_SHADOW_IN</property>
 306
 307                       <child>
 308                         <widget class="GtkNotebook" id="SequentsNotebook">
 309                           <property name="visible">True</property>
 310                           <property name="can_focus">True</property>
 311                           <property name="show_tabs">True</property>
 312                           <property name="show_border">True</property>
 313                           <property name="tab_pos">GTK_POS_TOP</property>
 314                           <property name="scrollable">False</property>
 315                           <property name="enable_popup">False</property>
 316                         </widget>
 317                       </child>
 318                     </widget>
 319                   </child>
 320                 </widget>
 321                 <packing>
 322                   <property name="shrink">True</property>
 323                   <property name="resize">False</property>
 324                 </packing>
 325               </child>
 326
 327               <child>
 328                 <widget class="GtkEventBox" id="ConsoleEventBox">
 329                   <property name="visible">True</property>
 330                   <property name="visible_window">True</property>
 331                   <property name="above_child">False</property>
 332
 333                   <child>
 334                     <widget class="GtkScrolledWindow" id="ScrolledConsole">
 335                       <property name="visible">True</property>
 336                       <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
 337                       <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
 338                       <property name="shadow_type">GTK_SHADOW_IN</property>
 339                       <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 340
 341                       <child>
 342                         <placeholder/>
 343                       </child>
 344                     </widget>
 345                   </child>
 346                 </widget>
 347                 <packing>
 348                   <property name="shrink">True</property>
 349                   <property name="resize">True</property>
 350                 </packing>
 351               </child>
 352             </widget>
 353             <packing>
 354               <property name="padding">0</property>
 355               <property name="expand">True</property>
 356               <property name="fill">True</property>
 357             </packing>
 358           </child>
 359
 360           <child>
 361             <widget class="GtkStatusbar" id="MainStatusBar">
 362               <property name="visible">True</property>
 363               <property name="has_resize_grip">True</property>
 364             </widget>
 365             <packing>
 366               <property name="padding">0</property>
 367               <property name="expand">False</property>
 368               <property name="fill">False</property>
 369             </packing>
 370           </child>
 371         </widget>
 372       </child>
 373     </widget>
 374   </child>
 375 </widget>
 376
 377 <widget class="GtkWindow" id="ProofWin">
 378   <property name="title" translatable="yes">Matita: current proof</property>
 379   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 380   <property name="window_position">GTK_WIN_POS_NONE</property>
 381   <property name="modal">False</property>
 382   <property name="default_width">700</property>
 383   <property name="default_height">525</property>
 384   <property name="resizable">True</property>
 385   <property name="destroy_with_parent">False</property>
 386   <property name="decorated">True</property>
 387   <property name="skip_taskbar_hint">False</property>
 388   <property name="skip_pager_hint">False</property>
 389   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
 390   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 391
 392   <child>
 393     <widget class="GtkEventBox" id="ProofWinEventBox">
 394       <property name="visible">True</property>
 395       <property name="visible_window">True</property>
 396       <property name="above_child">False</property>
 397
 398       <child>
 399         <widget class="GtkScrolledWindow" id="ScrolledProof">
 400           <property name="visible">True</property>
 401           <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
 402           <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
 403           <property name="shadow_type">GTK_SHADOW_NONE</property>
 404           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 405
 406           <child>
 407             <placeholder/>
 408           </child>
 409         </widget>
 410       </child>
 411     </widget>
 412   </child>
 413 </widget>
 414
 415 <widget class="GtkFileSelection" id="FileSelectionWin">
 416   <property name="border_width">10</property>
 417   <property name="title" translatable="yes">Select File</property>
 418   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 419   <property name="window_position">GTK_WIN_POS_CENTER</property>
 420   <property name="modal">True</property>
 421   <property name="resizable">True</property>
 422   <property name="destroy_with_parent">False</property>
 423   <property name="decorated">True</property>
 424   <property name="skip_taskbar_hint">False</property>
 425   <property name="skip_pager_hint">False</property>
 426   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 427   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 428   <property name="show_fileops">True</property>
 429
 430   <child internal-child="cancel_button">
 431     <widget class="GtkButton" id="fileSelCancelButton">
 432       <property name="visible">True</property>
 433       <property name="can_default">True</property>
 434       <property name="can_focus">True</property>
 435       <property name="relief">GTK_RELIEF_NORMAL</property>
 436       <property name="focus_on_click">True</property>
 437     </widget>
 438   </child>
 439
 440   <child internal-child="ok_button">
 441     <widget class="GtkButton" id="fileSelOkButton">
 442       <property name="visible">True</property>
 443       <property name="can_default">True</property>
 444       <property name="can_focus">True</property>
 445       <property name="relief">GTK_RELIEF_NORMAL</property>
 446       <property name="focus_on_click">True</property>
 447     </widget>
 448   </child>
 449 </widget>
 450
 451 <widget class="GtkWindow" id="ToolBarWin">
 452   <property name="width_request">130</property>
 453   <property name="height_request">450</property>
 454   <property name="visible">True</property>
 455   <property name="title" translatable="yes">ToolBar</property>
 456   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 457   <property name="window_position">GTK_WIN_POS_NONE</property>
 458   <property name="modal">False</property>
 459   <property name="resizable">False</property>
 460   <property name="destroy_with_parent">False</property>
 461   <property name="decorated">True</property>
 462   <property name="skip_taskbar_hint">False</property>
 463   <property name="skip_pager_hint">False</property>
 464   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
 465   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 466
 467   <child>
 468     <widget class="GtkEventBox" id="ToolBarEventBox">
 469       <property name="visible">True</property>
 470       <property name="visible_window">True</property>
 471       <property name="above_child">False</property>
 472
 473       <child>
 474         <widget class="GtkVBox" id="vbox1">
 475           <property name="visible">True</property>
 476           <property name="homogeneous">False</property>
 477           <property name="spacing">0</property>
 478
 479           <child>
 480             <widget class="GtkVButtonBox" id="vbuttonbox1">
 481               <property name="visible">True</property>
 482               <property name="layout_style">GTK_BUTTONBOX_DEFAULT_STYLE</property>
 483               <property name="spacing">0</property>
 484
 485               <child>
 486                 <widget class="GtkButton" id="button1">
 487                   <property name="width_request">120</property>
 488                   <property name="visible">True</property>
 489                   <property name="can_default">True</property>
 490                   <property name="can_focus">True</property>
 491                   <property name="label" translatable="yes">button1</property>
 492                   <property name="use_underline">True</property>
 493                   <property name="relief">GTK_RELIEF_NORMAL</property>
 494                   <property name="focus_on_click">True</property>
 495                 </widget>
 496               </child>
 497
 498               <child>
 499                 <widget class="GtkButton" id="button2">
 500                   <property name="visible">True</property>
 501                   <property name="can_default">True</property>
 502                   <property name="can_focus">True</property>
 503                   <property name="label" translatable="yes">button2</property>
 504                   <property name="use_underline">True</property>
 505                   <property name="relief">GTK_RELIEF_NORMAL</property>
 506                   <property name="focus_on_click">True</property>
 507                 </widget>
 508               </child>
 509
 510               <child>
 511                 <widget class="GtkButton" id="button3">
 512                   <property name="visible">True</property>
 513                   <property name="can_default">True</property>
 514                   <property name="can_focus">True</property>
 515                   <property name="label" translatable="yes">button3</property>
 516                   <property name="use_underline">True</property>
 517                   <property name="relief">GTK_RELIEF_NORMAL</property>
 518                   <property name="focus_on_click">True</property>
 519                 </widget>
 520               </child>
 521
 522               <child>
 523                 <widget class="GtkButton" id="button4">
 524                   <property name="visible">True</property>
 525                   <property name="can_default">True</property>
 526                   <property name="can_focus">True</property>
 527                   <property name="label" translatable="yes">button4</property>
 528                   <property name="use_underline">True</property>
 529                   <property name="relief">GTK_RELIEF_NORMAL</property>
 530                   <property name="focus_on_click">True</property>
 531                 </widget>
 532               </child>
 533             </widget>
 534             <packing>
 535               <property name="padding">0</property>
 536               <property name="expand">False</property>
 537               <property name="fill">True</property>
 538             </packing>
 539           </child>
 540
 541           <child>
 542             <widget class="GtkHSeparator" id="hseparator1">
 543               <property name="visible">True</property>
 544             </widget>
 545             <packing>
 546               <property name="padding">5</property>
 547               <property name="expand">False</property>
 548               <property name="fill">True</property>
 549             </packing>
 550           </child>
 551
 552           <child>
 553             <placeholder/>
 554           </child>
 555         </widget>
 556       </child>
 557     </widget>
 558   </child>
 559 </widget>
 560
 561 <widget class="GtkDialog" id="ConfirmationDialog">
 562   <property name="title" translatable="yes">DUMMY</property>
 563   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 564   <property name="window_position">GTK_WIN_POS_CENTER</property>
 565   <property name="modal">True</property>
 566   <property name="resizable">False</property>
 567   <property name="destroy_with_parent">False</property>
 568   <property name="decorated">True</property>
 569   <property name="skip_taskbar_hint">False</property>
 570   <property name="skip_pager_hint">False</property>
 571   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 572   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 573   <property name="has_separator">True</property>
 574
 575   <child internal-child="vbox">
 576     <widget class="GtkVBox" id="dialog-vbox1">
 577       <property name="visible">True</property>
 578       <property name="homogeneous">False</property>
 579       <property name="spacing">0</property>
 580
 581       <child internal-child="action_area">
 582         <widget class="GtkHButtonBox" id="dialog-action_area1">
 583           <property name="visible">True</property>
 584           <property name="layout_style">GTK_BUTTONBOX_END</property>
 585
 586           <child>
 587             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
 588               <property name="visible">True</property>
 589               <property name="can_default">True</property>
 590               <property name="can_focus">True</property>
 591               <property name="label">gtk-cancel</property>
 592               <property name="use_stock">True</property>
 593               <property name="relief">GTK_RELIEF_NORMAL</property>
 594               <property name="focus_on_click">True</property>
 595               <property name="response_id">-6</property>
 596             </widget>
 597           </child>
 598
 599           <child>
 600             <widget class="GtkButton" id="ConfirmationDialogOkButton">
 601               <property name="visible">True</property>
 602               <property name="can_default">True</property>
 603               <property name="can_focus">True</property>
 604               <property name="label">gtk-ok</property>
 605               <property name="use_stock">True</property>
 606               <property name="relief">GTK_RELIEF_NORMAL</property>
 607               <property name="focus_on_click">True</property>
 608               <property name="response_id">-5</property>
 609             </widget>
 610           </child>
 611         </widget>
 612         <packing>
 613           <property name="padding">0</property>
 614           <property name="expand">False</property>
 615           <property name="fill">True</property>
 616           <property name="pack_type">GTK_PACK_END</property>
 617         </packing>
 618       </child>
 619
 620       <child>
 621         <widget class="GtkLabel" id="ConfirmationDialogLabel">
 622           <property name="visible">True</property>
 623           <property name="label" translatable="yes">DUMMY</property>
 624           <property name="use_underline">False</property>
 625           <property name="use_markup">False</property>
 626           <property name="justify">GTK_JUSTIFY_CENTER</property>
 627           <property name="wrap">False</property>
 628           <property name="selectable">False</property>
 629           <property name="xalign">0.5</property>
 630           <property name="yalign">0.5</property>
 631           <property name="xpad">0</property>
 632           <property name="ypad">0</property>
 633         </widget>
 634         <packing>
 635           <property name="padding">0</property>
 636           <property name="expand">False</property>
 637           <property name="fill">False</property>
 638         </packing>
 639       </child>
 640     </widget>
 641   </child>
 642 </widget>
 643
 644 <widget class="GtkDialog" id="AboutWin">
 645   <property name="title" translatable="yes">Matita: about</property>
 646   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 647   <property name="window_position">GTK_WIN_POS_CENTER</property>
 648   <property name="modal">True</property>
 649   <property name="resizable">False</property>
 650   <property name="destroy_with_parent">False</property>
 651   <property name="decorated">True</property>
 652   <property name="skip_taskbar_hint">False</property>
 653   <property name="skip_pager_hint">False</property>
 654   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 655   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 656   <property name="has_separator">True</property>
 657
 658   <child internal-child="vbox">
 659     <widget class="GtkVBox" id="dialog-vbox2">
 660       <property name="visible">True</property>
 661       <property name="homogeneous">False</property>
 662       <property name="spacing">0</property>
 663
 664       <child internal-child="action_area">
 665         <widget class="GtkHButtonBox" id="dialog-action_area2">
 666           <property name="visible">True</property>
 667           <property name="layout_style">GTK_BUTTONBOX_END</property>
 668
 669           <child>
 670             <widget class="GtkButton" id="AboutDismissButton">
 671               <property name="visible">True</property>
 672               <property name="can_default">True</property>
 673               <property name="can_focus">True</property>
 674               <property name="label">gtk-ok</property>
 675               <property name="use_stock">True</property>
 676               <property name="relief">GTK_RELIEF_NORMAL</property>
 677               <property name="focus_on_click">True</property>
 678               <property name="response_id">-5</property>
 679             </widget>
 680           </child>
 681         </widget>
 682         <packing>
 683           <property name="padding">0</property>
 684           <property name="expand">False</property>
 685           <property name="fill">True</property>
 686           <property name="pack_type">GTK_PACK_END</property>
 687         </packing>
 688       </child>
 689
 690       <child>
 691         <widget class="GtkLabel" id="AboutLabel">
 692           <property name="visible">True</property>
 693           <property name="label" translatable="yes">&lt;b&gt;Matita @VERSION@&lt;/b&gt;
 694
 695 &lt;tt&gt;http://helm.cs.unibo.it&lt;/tt&gt;
 696
 697 Copyright (C) 2004,
 698 &lt;i&gt;the HELM team&lt;/i&gt;</property>
 699           <property name="use_underline">False</property>
 700           <property name="use_markup">True</property>
 701           <property name="justify">GTK_JUSTIFY_CENTER</property>
 702           <property name="wrap">False</property>
 703           <property name="selectable">False</property>
 704           <property name="xalign">0.5</property>
 705           <property name="yalign">0.5</property>
 706           <property name="xpad">5</property>
 707           <property name="ypad">5</property>
 708         </widget>
 709         <packing>
 710           <property name="padding">0</property>
 711           <property name="expand">False</property>
 712           <property name="fill">False</property>
 713         </packing>
 714       </child>
 715     </widget>
 716   </child>
 717 </widget>
 718
 719 <widget class="GtkDialog" id="UriChoiceDialog">
 720   <property name="height_request">280</property>
 721   <property name="title" translatable="yes">Uri choice</property>
 722   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 723   <property name="window_position">GTK_WIN_POS_CENTER</property>
 724   <property name="modal">True</property>
 725   <property name="resizable">True</property>
 726   <property name="destroy_with_parent">False</property>
 727   <property name="decorated">True</property>
 728   <property name="skip_taskbar_hint">False</property>
 729   <property name="skip_pager_hint">False</property>
 730   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 731   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 732   <property name="has_separator">True</property>
 733
 734   <child internal-child="vbox">
 735     <widget class="GtkVBox" id="dialog-vbox3">
 736       <property name="visible">True</property>
 737       <property name="homogeneous">False</property>
 738       <property name="spacing">0</property>
 739
 740       <child internal-child="action_area">
 741         <widget class="GtkHButtonBox" id="dialog-action_area3">
 742           <property name="visible">True</property>
 743           <property name="layout_style">GTK_BUTTONBOX_END</property>
 744
 745           <child>
 746             <widget class="GtkButton" id="UriChoiceAbortButton">
 747               <property name="visible">True</property>
 748               <property name="can_default">True</property>
 749               <property name="can_focus">True</property>
 750               <property name="label">gtk-cancel</property>
 751               <property name="use_stock">True</property>
 752               <property name="relief">GTK_RELIEF_NORMAL</property>
 753               <property name="focus_on_click">True</property>
 754               <property name="response_id">-6</property>
 755             </widget>
 756           </child>
 757
 758           <child>
 759             <widget class="GtkButton" id="UriChoiceSelectedButton">
 760               <property name="visible">True</property>
 761               <property name="can_default">True</property>
 762               <property name="can_focus">True</property>
 763               <property name="relief">GTK_RELIEF_NORMAL</property>
 764               <property name="focus_on_click">True</property>
 765               <property name="response_id">0</property>
 766
 767               <child>
 768                 <widget class="GtkAlignment" id="alignment2">
 769                   <property name="visible">True</property>
 770                   <property name="xalign">0.5</property>
 771                   <property name="yalign">0.5</property>
 772                   <property name="xscale">0</property>
 773                   <property name="yscale">0</property>
 774                   <property name="top_padding">0</property>
 775                   <property name="bottom_padding">0</property>
 776                   <property name="left_padding">0</property>
 777                   <property name="right_padding">0</property>
 778
 779                   <child>
 780                     <widget class="GtkHBox" id="hbox3">
 781                       <property name="visible">True</property>
 782                       <property name="homogeneous">False</property>
 783                       <property name="spacing">2</property>
 784
 785                       <child>
 786                         <widget class="GtkImage" id="image19">
 787                           <property name="visible">True</property>
 788                           <property name="stock">gtk-index</property>
 789                           <property name="icon_size">4</property>
 790                           <property name="xalign">0.5</property>
 791                           <property name="yalign">0.5</property>
 792                           <property name="xpad">0</property>
 793                           <property name="ypad">0</property>
 794                         </widget>
 795                         <packing>
 796                           <property name="padding">0</property>
 797                           <property name="expand">False</property>
 798                           <property name="fill">False</property>
 799                         </packing>
 800                       </child>
 801
 802                       <child>
 803                         <widget class="GtkLabel" id="label3">
 804                           <property name="visible">True</property>
 805                           <property name="label" translatable="yes">Try _Selected</property>
 806                           <property name="use_underline">True</property>
 807                           <property name="use_markup">False</property>
 808                           <property name="justify">GTK_JUSTIFY_LEFT</property>
 809                           <property name="wrap">False</property>
 810                           <property name="selectable">False</property>
 811                           <property name="xalign">0.5</property>
 812                           <property name="yalign">0.5</property>
 813                           <property name="xpad">0</property>
 814                           <property name="ypad">0</property>
 815                         </widget>
 816                         <packing>
 817                           <property name="padding">0</property>
 818                           <property name="expand">False</property>
 819                           <property name="fill">False</property>
 820                         </packing>
 821                       </child>
 822                     </widget>
 823                   </child>
 824                 </widget>
 825               </child>
 826             </widget>
 827           </child>
 828
 829           <child>
 830             <widget class="GtkButton" id="UriChoiceConstantsButton">
 831               <property name="visible">True</property>
 832               <property name="sensitive">False</property>
 833               <property name="can_default">True</property>
 834               <property name="can_focus">True</property>
 835               <property name="label" translatable="yes">Try Constants</property>
 836               <property name="use_underline">True</property>
 837               <property name="relief">GTK_RELIEF_NORMAL</property>
 838               <property name="focus_on_click">True</property>
 839               <property name="response_id">0</property>
 840             </widget>
 841           </child>
 842
 843           <child>
 844             <widget class="GtkButton" id="UriChoiceAutoButton">
 845               <property name="visible">True</property>
 846               <property name="can_default">True</property>
 847               <property name="can_focus">True</property>
 848               <property name="relief">GTK_RELIEF_NORMAL</property>
 849               <property name="focus_on_click">True</property>
 850               <property name="response_id">0</property>
 851
 852               <child>
 853                 <widget class="GtkAlignment" id="alignment1">
 854                   <property name="visible">True</property>
 855                   <property name="xalign">0.5</property>
 856                   <property name="yalign">0.5</property>
 857                   <property name="xscale">0</property>
 858                   <property name="yscale">0</property>
 859                   <property name="top_padding">0</property>
 860                   <property name="bottom_padding">0</property>
 861                   <property name="left_padding">0</property>
 862                   <property name="right_padding">0</property>
 863
 864                   <child>
 865                     <widget class="GtkHBox" id="hbox1">
 866                       <property name="visible">True</property>
 867                       <property name="homogeneous">False</property>
 868                       <property name="spacing">2</property>
 869
 870                       <child>
 871                         <widget class="GtkImage" id="image18">
 872                           <property name="visible">True</property>
 873                           <property name="stock">gtk-ok</property>
 874                           <property name="icon_size">4</property>
 875                           <property name="xalign">0.5</property>
 876                           <property name="yalign">0.5</property>
 877                           <property name="xpad">0</property>
 878                           <property name="ypad">0</property>
 879                         </widget>
 880                         <packing>
 881                           <property name="padding">0</property>
 882                           <property name="expand">False</property>
 883                           <property name="fill">False</property>
 884                         </packing>
 885                       </child>
 886
 887                       <child>
 888                         <widget class="GtkLabel" id="label1">
 889                           <property name="visible">True</property>
 890                           <property name="label" translatable="yes">_Auto</property>
 891                           <property name="use_underline">True</property>
 892                           <property name="use_markup">False</property>
 893                           <property name="justify">GTK_JUSTIFY_LEFT</property>
 894                           <property name="wrap">False</property>
 895                           <property name="selectable">False</property>
 896                           <property name="xalign">0.5</property>
 897                           <property name="yalign">0.5</property>
 898                           <property name="xpad">0</property>
 899                           <property name="ypad">0</property>
 900                         </widget>
 901                         <packing>
 902                           <property name="padding">0</property>
 903                           <property name="expand">False</property>
 904                           <property name="fill">False</property>
 905                         </packing>
 906                       </child>
 907                     </widget>
 908                   </child>
 909                 </widget>
 910               </child>
 911             </widget>
 912           </child>
 913         </widget>
 914         <packing>
 915           <property name="padding">0</property>
 916           <property name="expand">False</property>
 917           <property name="fill">True</property>
 918           <property name="pack_type">GTK_PACK_END</property>
 919         </packing>
 920       </child>
 921
 922       <child>
 923         <widget class="GtkVBox" id="vbox2">
 924           <property name="visible">True</property>
 925           <property name="homogeneous">False</property>
 926           <property name="spacing">0</property>
 927
 928           <child>
 929             <widget class="GtkLabel" id="UriChoiceLabel">
 930               <property name="visible">True</property>
 931               <property name="label" translatable="yes">some informative message here ...</property>
 932               <property name="use_underline">False</property>
 933               <property name="use_markup">False</property>
 934               <property name="justify">GTK_JUSTIFY_LEFT</property>
 935               <property name="wrap">False</property>
 936               <property name="selectable">False</property>
 937               <property name="xalign">0.5</property>
 938               <property name="yalign">0.5</property>
 939               <property name="xpad">0</property>
 940               <property name="ypad">0</property>
 941             </widget>
 942             <packing>
 943               <property name="padding">0</property>
 944               <property name="expand">False</property>
 945               <property name="fill">False</property>
 946             </packing>
 947           </child>
 948
 949           <child>
 950             <widget class="GtkScrolledWindow" id="scrolledwindow1">
 951               <property name="visible">True</property>
 952               <property name="can_focus">True</property>
 953               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
 954               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
 955               <property name="shadow_type">GTK_SHADOW_NONE</property>
 956               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 957
 958               <child>
 959                 <widget class="GtkTreeView" id="UriChoiceTreeView">
 960                   <property name="visible">True</property>
 961                   <property name="can_focus">True</property>
 962                   <property name="headers_visible">False</property>
 963                   <property name="rules_hint">False</property>
 964                   <property name="reorderable">False</property>
 965                   <property name="enable_search">True</property>
 966                 </widget>
 967               </child>
 968             </widget>
 969             <packing>
 970               <property name="padding">0</property>
 971               <property name="expand">True</property>
 972               <property name="fill">True</property>
 973             </packing>
 974           </child>
 975
 976           <child>
 977             <widget class="GtkHBox" id="hbox2">
 978               <property name="visible">True</property>
 979               <property name="homogeneous">False</property>
 980               <property name="spacing">0</property>
 981
 982               <child>
 983                 <widget class="GtkLabel" id="label2">
 984                   <property name="visible">True</property>
 985                   <property name="label" translatable="yes">URI: </property>
 986                   <property name="use_underline">False</property>
 987                   <property name="use_markup">False</property>
 988                   <property name="justify">GTK_JUSTIFY_LEFT</property>
 989                   <property name="wrap">False</property>
 990                   <property name="selectable">False</property>
 991                   <property name="xalign">0.5</property>
 992                   <property name="yalign">0.5</property>
 993                   <property name="xpad">0</property>
 994                   <property name="ypad">0</property>
 995                 </widget>
 996                 <packing>
 997                   <property name="padding">0</property>
 998                   <property name="expand">False</property>
 999                   <property name="fill">False</property>
1000                 </packing>
1001               </child>
1002
1003               <child>
1004                 <widget class="GtkEntry" id="entry1">
1005                   <property name="visible">True</property>
1006                   <property name="can_focus">True</property>
1007                   <property name="editable">True</property>
1008                   <property name="visibility">True</property>
1009                   <property name="max_length">0</property>
1010                   <property name="text" translatable="yes"></property>
1011                   <property name="has_frame">True</property>
1012                   <property name="invisible_char">*</property>
1013                   <property name="activates_default">False</property>
1014                 </widget>
1015                 <packing>
1016                   <property name="padding">0</property>
1017                   <property name="expand">True</property>
1018                   <property name="fill">True</property>
1019                 </packing>
1020               </child>
1021             </widget>
1022             <packing>
1023               <property name="padding">0</property>
1024               <property name="expand">False</property>
1025               <property name="fill">True</property>
1026             </packing>
1027           </child>
1028         </widget>
1029         <packing>
1030           <property name="padding">0</property>
1031           <property name="expand">True</property>
1032           <property name="fill">True</property>
1033         </packing>
1034       </child>
1035     </widget>
1036   </child>
1037 </widget>
1038
1039 <widget class="GtkDialog" id="InterpChoiceDialog">
1040   <property name="title" translatable="yes">Interpretation choice</property>
1041   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1042   <property name="window_position">GTK_WIN_POS_NONE</property>
1043   <property name="modal">True</property>
1044   <property name="resizable">True</property>
1045   <property name="destroy_with_parent">False</property>
1046   <property name="decorated">True</property>
1047   <property name="skip_taskbar_hint">False</property>
1048   <property name="skip_pager_hint">False</property>
1049   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1050   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1051   <property name="has_separator">True</property>
1052
1053   <child internal-child="vbox">
1054     <widget class="GtkVBox" id="dialog-vbox4">
1055       <property name="visible">True</property>
1056       <property name="homogeneous">False</property>
1057       <property name="spacing">0</property>
1058
1059       <child internal-child="action_area">
1060         <widget class="GtkHButtonBox" id="dialog-action_area4">
1061           <property name="visible">True</property>
1062           <property name="layout_style">GTK_BUTTONBOX_END</property>
1063
1064           <child>
1065             <widget class="GtkButton" id="InterpChoiceHelpButton">
1066               <property name="visible">True</property>
1067               <property name="can_default">True</property>
1068               <property name="can_focus">True</property>
1069               <property name="label">gtk-help</property>
1070               <property name="use_stock">True</property>
1071               <property name="relief">GTK_RELIEF_NORMAL</property>
1072               <property name="focus_on_click">True</property>
1073               <property name="response_id">-11</property>
1074             </widget>
1075           </child>
1076
1077           <child>
1078             <widget class="GtkButton" id="InterpChoiceCancelButton">
1079               <property name="visible">True</property>
1080               <property name="can_default">True</property>
1081               <property name="can_focus">True</property>
1082               <property name="label">gtk-cancel</property>
1083               <property name="use_stock">True</property>
1084               <property name="relief">GTK_RELIEF_NORMAL</property>
1085               <property name="focus_on_click">True</property>
1086               <property name="response_id">-6</property>
1087             </widget>
1088           </child>
1089
1090           <child>
1091             <widget class="GtkButton" id="InterpChoiceOkButton">
1092               <property name="visible">True</property>
1093               <property name="can_default">True</property>
1094               <property name="can_focus">True</property>
1095               <property name="label">gtk-ok</property>
1096               <property name="use_stock">True</property>
1097               <property name="relief">GTK_RELIEF_NORMAL</property>
1098               <property name="focus_on_click">True</property>
1099               <property name="response_id">-5</property>
1100             </widget>
1101           </child>
1102         </widget>
1103         <packing>
1104           <property name="padding">0</property>
1105           <property name="expand">False</property>
1106           <property name="fill">True</property>
1107           <property name="pack_type">GTK_PACK_END</property>
1108         </packing>
1109       </child>
1110
1111       <child>
1112         <widget class="GtkVBox" id="vbox3">
1113           <property name="visible">True</property>
1114           <property name="homogeneous">False</property>
1115           <property name="spacing">0</property>
1116
1117           <child>
1118             <widget class="GtkLabel" id="label6">
1119               <property name="visible">True</property>
1120               <property name="label" translatable="yes">some informative message here ...</property>
1121               <property name="use_underline">False</property>
1122               <property name="use_markup">False</property>
1123               <property name="justify">GTK_JUSTIFY_LEFT</property>
1124               <property name="wrap">False</property>
1125               <property name="selectable">False</property>
1126               <property name="xalign">0.5</property>
1127               <property name="yalign">0.5</property>
1128               <property name="xpad">0</property>
1129               <property name="ypad">0</property>
1130             </widget>
1131             <packing>
1132               <property name="padding">0</property>
1133               <property name="expand">False</property>
1134               <property name="fill">False</property>
1135             </packing>
1136           </child>
1137
1138           <child>
1139             <placeholder/>
1140           </child>
1141         </widget>
1142         <packing>
1143           <property name="padding">0</property>
1144           <property name="expand">True</property>
1145           <property name="fill">True</property>
1146         </packing>
1147       </child>
1148     </widget>
1149   </child>
1150 </widget>
1151
1152 <widget class="GtkDialog" id="EmptyDialog">
1153   <property name="visible">True</property>
1154   <property name="title" translatable="yes">DUMMY</property>
1155   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1156   <property name="window_position">GTK_WIN_POS_NONE</property>
1157   <property name="modal">False</property>
1158   <property name="resizable">True</property>
1159   <property name="destroy_with_parent">False</property>
1160   <property name="decorated">True</property>
1161   <property name="skip_taskbar_hint">False</property>
1162   <property name="skip_pager_hint">False</property>
1163   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1164   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1165   <property name="has_separator">True</property>
1166
1167   <child internal-child="vbox">
1168     <widget class="GtkVBox" id="EmptyDialogVBox">
1169       <property name="visible">True</property>
1170       <property name="homogeneous">False</property>
1171       <property name="spacing">0</property>
1172
1173       <child internal-child="action_area">
1174         <widget class="GtkHButtonBox" id="dialog-action_area5">
1175           <property name="visible">True</property>
1176           <property name="layout_style">GTK_BUTTONBOX_END</property>
1177
1178           <child>
1179             <widget class="GtkButton" id="EmptyDialogCancelButton">
1180               <property name="visible">True</property>
1181               <property name="can_default">True</property>
1182               <property name="can_focus">True</property>
1183               <property name="label">gtk-cancel</property>
1184               <property name="use_stock">True</property>
1185               <property name="relief">GTK_RELIEF_NORMAL</property>
1186               <property name="focus_on_click">True</property>
1187               <property name="response_id">-6</property>
1188             </widget>
1189           </child>
1190
1191           <child>
1192             <widget class="GtkButton" id="EmptyDialogOkButton">
1193               <property name="visible">True</property>
1194               <property name="can_default">True</property>
1195               <property name="can_focus">True</property>
1196               <property name="label">gtk-ok</property>
1197               <property name="use_stock">True</property>
1198               <property name="relief">GTK_RELIEF_NORMAL</property>
1199               <property name="focus_on_click">True</property>
1200               <property name="response_id">-5</property>
1201             </widget>
1202           </child>
1203         </widget>
1204         <packing>
1205           <property name="padding">0</property>
1206           <property name="expand">False</property>
1207           <property name="fill">True</property>
1208           <property name="pack_type">GTK_PACK_END</property>
1209         </packing>
1210       </child>
1211
1212       <child>
1213         <widget class="GtkLabel" id="EmptyDialogLabel">
1214           <property name="visible">True</property>
1215           <property name="label" translatable="yes">DUMMY</property>
1216           <property name="use_underline">False</property>
1217           <property name="use_markup">False</property>
1218           <property name="justify">GTK_JUSTIFY_LEFT</property>
1219           <property name="wrap">False</property>
1220           <property name="selectable">False</property>
1221           <property name="xalign">0.5</property>
1222           <property name="yalign">0.5</property>
1223           <property name="xpad">0</property>
1224           <property name="ypad">0</property>
1225         </widget>
1226         <packing>
1227           <property name="padding">0</property>
1228           <property name="expand">False</property>
1229           <property name="fill">False</property>
1230         </packing>
1231       </child>
1232
1233       <child>
1234         <placeholder/>
1235       </child>
1236     </widget>
1237   </child>
1238 </widget>
1239
1240 <widget class="GtkWindow" id="CheckWin">
1241   <property name="width_request">300</property>
1242   <property name="height_request">200</property>
1243   <property name="title" translatable="yes">Matita: check term</property>
1244   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1245   <property name="window_position">GTK_WIN_POS_NONE</property>
1246   <property name="modal">False</property>
1247   <property name="resizable">True</property>
1248   <property name="destroy_with_parent">False</property>
1249   <property name="decorated">True</property>
1250   <property name="skip_taskbar_hint">False</property>
1251   <property name="skip_pager_hint">False</property>
1252   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1253   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1254
1255   <child>
1256     <widget class="GtkEventBox" id="CheckWinEventBox">
1257       <property name="visible">True</property>
1258       <property name="visible_window">True</property>
1259       <property name="above_child">False</property>
1260
1261       <child>
1262         <widget class="GtkScrolledWindow" id="ScrolledCheck">
1263           <property name="visible">True</property>
1264           <property name="can_focus">True</property>
1265           <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1266           <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1267           <property name="shadow_type">GTK_SHADOW_NONE</property>
1268           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1269
1270           <child>
1271             <placeholder/>
1272           </child>
1273         </widget>
1274       </child>
1275     </widget>
1276   </child>
1277 </widget>
1278
1279 <widget class="GtkWindow" id="ScriptWin">
1280   <property name="title" translatable="yes">Matita: script</property>
1281   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1282   <property name="window_position">GTK_WIN_POS_NONE</property>
1283   <property name="modal">False</property>
1284   <property name="default_width">450</property>
1285   <property name="default_height">800</property>
1286   <property name="resizable">True</property>
1287   <property name="destroy_with_parent">False</property>
1288   <property name="decorated">True</property>
1289   <property name="skip_taskbar_hint">False</property>
1290   <property name="skip_pager_hint">False</property>
1291   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1292   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1293
1294   <child>
1295     <widget class="GtkEventBox" id="ScriptWinEventBox">
1296       <property name="visible">True</property>
1297       <property name="visible_window">True</property>
1298       <property name="above_child">False</property>
1299
1300       <child>
1301         <widget class="GtkVBox" id="vbox4">
1302           <property name="visible">True</property>
1303           <property name="homogeneous">False</property>
1304           <property name="spacing">0</property>
1305
1306           <child>
1307             <widget class="GtkToolbar" id="toolbar1">
1308               <property name="visible">True</property>
1309               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1310               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1311               <property name="tooltips">True</property>
1312               <property name="show_arrow">True</property>
1313
1314               <child>
1315                 <widget class="GtkToolItem" id="toolitem1">
1316                   <property name="visible">True</property>
1317                   <property name="visible_horizontal">True</property>
1318                   <property name="visible_vertical">True</property>
1319                   <property name="is_important">False</property>
1320
1321                   <child>
1322                     <widget class="GtkButton" id="button5">
1323                       <property name="visible">True</property>
1324                       <property name="tooltip" translatable="yes">go back 1 phrase</property>
1325                       <property name="can_focus">True</property>
1326                       <property name="relief">GTK_RELIEF_NORMAL</property>
1327                       <property name="focus_on_click">True</property>
1328
1329                       <child>
1330                         <widget class="GtkImage" id="image133">
1331                           <property name="visible">True</property>
1332                           <property name="stock">gtk-go-back</property>
1333                           <property name="icon_size">4</property>
1334                           <property name="xalign">0.5</property>
1335                           <property name="yalign">0.5</property>
1336                           <property name="xpad">0</property>
1337                           <property name="ypad">0</property>
1338                         </widget>
1339                       </child>
1340                     </widget>
1341                   </child>
1342                 </widget>
1343                 <packing>
1344                   <property name="expand">False</property>
1345                   <property name="homogeneous">False</property>
1346                 </packing>
1347               </child>
1348
1349               <child>
1350                 <widget class="GtkToolItem" id="toolitem2">
1351                   <property name="visible">True</property>
1352                   <property name="visible_horizontal">True</property>
1353                   <property name="visible_vertical">True</property>
1354                   <property name="is_important">False</property>
1355
1356                   <child>
1357                     <widget class="GtkButton" id="button6">
1358                       <property name="visible">True</property>
1359                       <property name="tooltip" translatable="yes">execute til cursor</property>
1360                       <property name="can_focus">True</property>
1361                       <property name="relief">GTK_RELIEF_NORMAL</property>
1362                       <property name="focus_on_click">True</property>
1363
1364                       <child>
1365                         <widget class="GtkImage" id="image134">
1366                           <property name="visible">True</property>
1367                           <property name="stock">gtk-jump-to</property>
1368                           <property name="icon_size">4</property>
1369                           <property name="xalign">0.5</property>
1370                           <property name="yalign">0.5</property>
1371                           <property name="xpad">0</property>
1372                           <property name="ypad">0</property>
1373                         </widget>
1374                       </child>
1375                     </widget>
1376                   </child>
1377                 </widget>
1378                 <packing>
1379                   <property name="expand">False</property>
1380                   <property name="homogeneous">False</property>
1381                 </packing>
1382               </child>
1383
1384               <child>
1385                 <widget class="GtkToolItem" id="toolitem3">
1386                   <property name="visible">True</property>
1387                   <property name="visible_horizontal">True</property>
1388                   <property name="visible_vertical">True</property>
1389                   <property name="is_important">False</property>
1390
1391                   <child>
1392                     <widget class="GtkButton" id="button7">
1393                       <property name="visible">True</property>
1394                       <property name="tooltip" translatable="yes">go forward 1 phrase</property>
1395                       <property name="can_focus">True</property>
1396                       <property name="relief">GTK_RELIEF_NORMAL</property>
1397                       <property name="focus_on_click">True</property>
1398
1399                       <child>
1400                         <widget class="GtkImage" id="image135">
1401                           <property name="visible">True</property>
1402                           <property name="stock">gtk-go-forward</property>
1403                           <property name="icon_size">4</property>
1404                           <property name="xalign">0.5</property>
1405                           <property name="yalign">0.5</property>
1406                           <property name="xpad">0</property>
1407                           <property name="ypad">0</property>
1408                         </widget>
1409                       </child>
1410                     </widget>
1411                   </child>
1412                 </widget>
1413                 <packing>
1414                   <property name="expand">False</property>
1415                   <property name="homogeneous">False</property>
1416                 </packing>
1417               </child>
1418             </widget>
1419             <packing>
1420               <property name="padding">0</property>
1421               <property name="expand">False</property>
1422               <property name="fill">False</property>
1423             </packing>
1424           </child>
1425
1426           <child>
1427             <widget class="GtkScrolledWindow" id="ScrolledScript">
1428               <property name="visible">True</property>
1429               <property name="can_focus">True</property>
1430               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1431               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1432               <property name="shadow_type">GTK_SHADOW_NONE</property>
1433               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1434
1435               <child>
1436                 <widget class="GtkTextView" id="ScriptTextView">
1437                   <property name="visible">True</property>
1438                   <property name="can_focus">True</property>
1439                   <property name="editable">True</property>
1440                   <property name="overwrite">False</property>
1441                   <property name="accepts_tab">True</property>
1442                   <property name="justification">GTK_JUSTIFY_LEFT</property>
1443                   <property name="wrap_mode">GTK_WRAP_NONE</property>
1444                   <property name="cursor_visible">True</property>
1445                   <property name="pixels_above_lines">0</property>
1446                   <property name="pixels_below_lines">0</property>
1447                   <property name="pixels_inside_wrap">0</property>
1448                   <property name="left_margin">0</property>
1449                   <property name="right_margin">0</property>
1450                   <property name="indent">0</property>
1451                   <property name="text" translatable="yes"></property>
1452                 </widget>
1453               </child>
1454             </widget>
1455             <packing>
1456               <property name="padding">0</property>
1457               <property name="expand">True</property>
1458               <property name="fill">True</property>
1459             </packing>
1460           </child>
1461         </widget>
1462       </child>
1463     </widget>
1464   </child>
1465 </widget>
1466
1467 </glade-interface>