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">150</property>
 453   <property name="height_request">450</property>
 454   <property name="visible">True</property>
 455   <property name="title" translatable="yes">Tactics</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="ToolBarVBox">
 475           <property name="visible">True</property>
 476           <property name="homogeneous">False</property>
 477           <property name="spacing">0</property>
 478
 479           <child>
 480             <widget class="GtkToolbar" id="toolbar2">
 481               <property name="visible">True</property>
 482               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 483               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 484               <property name="tooltips">True</property>
 485               <property name="show_arrow">True</property>
 486
 487               <child>
 488                 <widget class="GtkToolItem" id="toolitem4">
 489                   <property name="visible">True</property>
 490                   <property name="visible_horizontal">True</property>
 491                   <property name="visible_vertical">True</property>
 492                   <property name="is_important">False</property>
 493
 494                   <child>
 495                     <widget class="GtkButton" id="introsButton">
 496                       <property name="visible">True</property>
 497                       <property name="tooltip" translatable="yes">Intros</property>
 498                       <property name="can_focus">True</property>
 499                       <property name="label" translatable="yes">intros</property>
 500                       <property name="use_underline">True</property>
 501                       <property name="relief">GTK_RELIEF_NORMAL</property>
 502                       <property name="focus_on_click">True</property>
 503                     </widget>
 504                   </child>
 505                 </widget>
 506                 <packing>
 507                   <property name="expand">False</property>
 508                   <property name="homogeneous">False</property>
 509                 </packing>
 510               </child>
 511
 512               <child>
 513                 <widget class="GtkToolItem" id="toolitem5">
 514                   <property name="visible">True</property>
 515                   <property name="visible_horizontal">True</property>
 516                   <property name="visible_vertical">True</property>
 517                   <property name="is_important">False</property>
 518
 519                   <child>
 520                     <widget class="GtkButton" id="applyButton">
 521                       <property name="visible">True</property>
 522                       <property name="tooltip" translatable="yes">Apply</property>
 523                       <property name="can_focus">True</property>
 524                       <property name="label" translatable="yes">apply</property>
 525                       <property name="use_underline">True</property>
 526                       <property name="relief">GTK_RELIEF_NORMAL</property>
 527                       <property name="focus_on_click">True</property>
 528                     </widget>
 529                   </child>
 530                 </widget>
 531                 <packing>
 532                   <property name="expand">False</property>
 533                   <property name="homogeneous">False</property>
 534                 </packing>
 535               </child>
 536
 537               <child>
 538                 <widget class="GtkToolItem" id="toolitem6">
 539                   <property name="visible">True</property>
 540                   <property name="visible_horizontal">True</property>
 541                   <property name="visible_vertical">True</property>
 542                   <property name="is_important">False</property>
 543
 544                   <child>
 545                     <widget class="GtkButton" id="exactButton">
 546                       <property name="visible">True</property>
 547                       <property name="tooltip" translatable="yes">Exact</property>
 548                       <property name="can_focus">True</property>
 549                       <property name="label" translatable="yes">exact</property>
 550                       <property name="use_underline">True</property>
 551                       <property name="relief">GTK_RELIEF_NORMAL</property>
 552                       <property name="focus_on_click">True</property>
 553                     </widget>
 554                   </child>
 555                 </widget>
 556                 <packing>
 557                   <property name="expand">False</property>
 558                   <property name="homogeneous">False</property>
 559                 </packing>
 560               </child>
 561             </widget>
 562             <packing>
 563               <property name="padding">0</property>
 564               <property name="expand">False</property>
 565               <property name="fill">False</property>
 566             </packing>
 567           </child>
 568
 569           <child>
 570             <widget class="GtkToolbar" id="toolbar3">
 571               <property name="visible">True</property>
 572               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 573               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 574               <property name="tooltips">True</property>
 575               <property name="show_arrow">True</property>
 576
 577               <child>
 578                 <widget class="GtkToolItem" id="toolitem7">
 579                   <property name="visible">True</property>
 580                   <property name="visible_horizontal">True</property>
 581                   <property name="visible_vertical">True</property>
 582                   <property name="is_important">False</property>
 583
 584                   <child>
 585                     <widget class="GtkButton" id="elimButton">
 586                       <property name="visible">True</property>
 587                       <property name="tooltip" translatable="yes">Elim</property>
 588                       <property name="can_focus">True</property>
 589                       <property name="label" translatable="yes">elim</property>
 590                       <property name="use_underline">True</property>
 591                       <property name="relief">GTK_RELIEF_NORMAL</property>
 592                       <property name="focus_on_click">True</property>
 593                     </widget>
 594                   </child>
 595                 </widget>
 596                 <packing>
 597                   <property name="expand">False</property>
 598                   <property name="homogeneous">False</property>
 599                 </packing>
 600               </child>
 601
 602               <child>
 603                 <widget class="GtkToolItem" id="toolitem8">
 604                   <property name="visible">True</property>
 605                   <property name="visible_horizontal">True</property>
 606                   <property name="visible_vertical">True</property>
 607                   <property name="is_important">False</property>
 608
 609                   <child>
 610                     <widget class="GtkButton" id="elimTypeButton">
 611                       <property name="visible">True</property>
 612                       <property name="tooltip" translatable="yes">ElimType</property>
 613                       <property name="can_focus">True</property>
 614                       <property name="label" translatable="yes">elimTy</property>
 615                       <property name="use_underline">True</property>
 616                       <property name="relief">GTK_RELIEF_NORMAL</property>
 617                       <property name="focus_on_click">True</property>
 618                     </widget>
 619                   </child>
 620                 </widget>
 621                 <packing>
 622                   <property name="expand">False</property>
 623                   <property name="homogeneous">False</property>
 624                 </packing>
 625               </child>
 626             </widget>
 627             <packing>
 628               <property name="padding">0</property>
 629               <property name="expand">False</property>
 630               <property name="fill">False</property>
 631             </packing>
 632           </child>
 633
 634           <child>
 635             <widget class="GtkToolbar" id="toolbar4">
 636               <property name="visible">True</property>
 637               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 638               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 639               <property name="tooltips">True</property>
 640               <property name="show_arrow">True</property>
 641
 642               <child>
 643                 <widget class="GtkToolItem" id="toolitem9">
 644                   <property name="visible">True</property>
 645                   <property name="visible_horizontal">True</property>
 646                   <property name="visible_vertical">True</property>
 647                   <property name="is_important">False</property>
 648
 649                   <child>
 650                     <widget class="GtkButton" id="splitButton">
 651                       <property name="visible">True</property>
 652                       <property name="tooltip" translatable="yes">Split</property>
 653                       <property name="can_focus">True</property>
 654                       <property name="label" translatable="yes">split</property>
 655                       <property name="use_underline">True</property>
 656                       <property name="relief">GTK_RELIEF_NORMAL</property>
 657                       <property name="focus_on_click">True</property>
 658                     </widget>
 659                   </child>
 660                 </widget>
 661                 <packing>
 662                   <property name="expand">False</property>
 663                   <property name="homogeneous">False</property>
 664                 </packing>
 665               </child>
 666
 667               <child>
 668                 <widget class="GtkToolItem" id="toolitem10">
 669                   <property name="visible">True</property>
 670                   <property name="visible_horizontal">True</property>
 671                   <property name="visible_vertical">True</property>
 672                   <property name="is_important">False</property>
 673
 674                   <child>
 675                     <widget class="GtkButton" id="leftButton">
 676                       <property name="visible">True</property>
 677                       <property name="tooltip" translatable="yes">Left</property>
 678                       <property name="can_focus">True</property>
 679                       <property name="label" translatable="yes">left</property>
 680                       <property name="use_underline">True</property>
 681                       <property name="relief">GTK_RELIEF_NORMAL</property>
 682                       <property name="focus_on_click">True</property>
 683                     </widget>
 684                   </child>
 685                 </widget>
 686                 <packing>
 687                   <property name="expand">False</property>
 688                   <property name="homogeneous">False</property>
 689                 </packing>
 690               </child>
 691
 692               <child>
 693                 <widget class="GtkToolItem" id="toolitem11">
 694                   <property name="visible">True</property>
 695                   <property name="visible_horizontal">True</property>
 696                   <property name="visible_vertical">True</property>
 697                   <property name="is_important">False</property>
 698
 699                   <child>
 700                     <widget class="GtkButton" id="rightButton">
 701                       <property name="visible">True</property>
 702                       <property name="tooltip" translatable="yes">Right</property>
 703                       <property name="can_focus">True</property>
 704                       <property name="label" translatable="yes">right</property>
 705                       <property name="use_underline">True</property>
 706                       <property name="relief">GTK_RELIEF_NORMAL</property>
 707                       <property name="focus_on_click">True</property>
 708                     </widget>
 709                   </child>
 710                 </widget>
 711                 <packing>
 712                   <property name="expand">False</property>
 713                   <property name="homogeneous">False</property>
 714                 </packing>
 715               </child>
 716
 717               <child>
 718                 <widget class="GtkToolItem" id="toolitem12">
 719                   <property name="visible">True</property>
 720                   <property name="visible_horizontal">True</property>
 721                   <property name="visible_vertical">True</property>
 722                   <property name="is_important">False</property>
 723
 724                   <child>
 725                     <widget class="GtkButton" id="existsButton">
 726                       <property name="visible">True</property>
 727                       <property name="tooltip" translatable="yes">Exists</property>
 728                       <property name="can_focus">True</property>
 729                       <property name="label" translatable="yes">∃</property>
 730                       <property name="use_underline">True</property>
 731                       <property name="relief">GTK_RELIEF_NORMAL</property>
 732                       <property name="focus_on_click">True</property>
 733                     </widget>
 734                   </child>
 735                 </widget>
 736                 <packing>
 737                   <property name="expand">False</property>
 738                   <property name="homogeneous">False</property>
 739                 </packing>
 740               </child>
 741             </widget>
 742             <packing>
 743               <property name="padding">0</property>
 744               <property name="expand">False</property>
 745               <property name="fill">False</property>
 746             </packing>
 747           </child>
 748
 749           <child>
 750             <widget class="GtkToolbar" id="toolbar5">
 751               <property name="visible">True</property>
 752               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 753               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 754               <property name="tooltips">True</property>
 755               <property name="show_arrow">True</property>
 756
 757               <child>
 758                 <widget class="GtkToolItem" id="toolitem14">
 759                   <property name="visible">True</property>
 760                   <property name="visible_horizontal">True</property>
 761                   <property name="visible_vertical">True</property>
 762                   <property name="is_important">False</property>
 763
 764                   <child>
 765                     <widget class="GtkButton" id="reflexivityButton">
 766                       <property name="visible">True</property>
 767                       <property name="tooltip" translatable="yes">Reflexivity</property>
 768                       <property name="can_focus">True</property>
 769                       <property name="label" translatable="yes">refl</property>
 770                       <property name="use_underline">True</property>
 771                       <property name="relief">GTK_RELIEF_NORMAL</property>
 772                       <property name="focus_on_click">True</property>
 773                     </widget>
 774                   </child>
 775                 </widget>
 776                 <packing>
 777                   <property name="expand">False</property>
 778                   <property name="homogeneous">False</property>
 779                 </packing>
 780               </child>
 781
 782               <child>
 783                 <widget class="GtkToolItem" id="toolitem15">
 784                   <property name="visible">True</property>
 785                   <property name="visible_horizontal">True</property>
 786                   <property name="visible_vertical">True</property>
 787                   <property name="is_important">False</property>
 788
 789                   <child>
 790                     <widget class="GtkButton" id="symmetryButton">
 791                       <property name="visible">True</property>
 792                       <property name="tooltip" translatable="yes">Symmetry</property>
 793                       <property name="can_focus">True</property>
 794                       <property name="label" translatable="yes">sym</property>
 795                       <property name="use_underline">True</property>
 796                       <property name="relief">GTK_RELIEF_NORMAL</property>
 797                       <property name="focus_on_click">True</property>
 798                     </widget>
 799                   </child>
 800                 </widget>
 801                 <packing>
 802                   <property name="expand">False</property>
 803                   <property name="homogeneous">False</property>
 804                 </packing>
 805               </child>
 806
 807               <child>
 808                 <widget class="GtkToolItem" id="toolitem16">
 809                   <property name="visible">True</property>
 810                   <property name="visible_horizontal">True</property>
 811                   <property name="visible_vertical">True</property>
 812                   <property name="is_important">False</property>
 813
 814                   <child>
 815                     <widget class="GtkButton" id="transitivityButton">
 816                       <property name="visible">True</property>
 817                       <property name="tooltip" translatable="yes">Transitivity</property>
 818                       <property name="can_focus">True</property>
 819                       <property name="label" translatable="yes">trans</property>
 820                       <property name="use_underline">True</property>
 821                       <property name="relief">GTK_RELIEF_NORMAL</property>
 822                       <property name="focus_on_click">True</property>
 823                     </widget>
 824                   </child>
 825                 </widget>
 826                 <packing>
 827                   <property name="expand">False</property>
 828                   <property name="homogeneous">False</property>
 829                 </packing>
 830               </child>
 831             </widget>
 832             <packing>
 833               <property name="padding">0</property>
 834               <property name="expand">False</property>
 835               <property name="fill">False</property>
 836             </packing>
 837           </child>
 838
 839           <child>
 840             <widget class="GtkToolbar" id="toolbar6">
 841               <property name="visible">True</property>
 842               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 843               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 844               <property name="tooltips">True</property>
 845               <property name="show_arrow">True</property>
 846
 847               <child>
 848                 <widget class="GtkToolItem" id="toolitem17">
 849                   <property name="visible">True</property>
 850                   <property name="visible_horizontal">True</property>
 851                   <property name="visible_vertical">True</property>
 852                   <property name="is_important">False</property>
 853
 854                   <child>
 855                     <widget class="GtkButton" id="assumptionButton">
 856                       <property name="visible">True</property>
 857                       <property name="tooltip" translatable="yes">Assumption</property>
 858                       <property name="can_focus">True</property>
 859                       <property name="label" translatable="yes">assum</property>
 860                       <property name="use_underline">True</property>
 861                       <property name="relief">GTK_RELIEF_NORMAL</property>
 862                       <property name="focus_on_click">True</property>
 863                     </widget>
 864                   </child>
 865                 </widget>
 866                 <packing>
 867                   <property name="expand">False</property>
 868                   <property name="homogeneous">False</property>
 869                 </packing>
 870               </child>
 871
 872               <child>
 873                 <widget class="GtkToolItem" id="toolitem18">
 874                   <property name="visible">True</property>
 875                   <property name="visible_horizontal">True</property>
 876                   <property name="visible_vertical">True</property>
 877                   <property name="is_important">False</property>
 878
 879                   <child>
 880                     <widget class="GtkButton" id="searchButton">
 881                       <property name="visible">True</property>
 882                       <property name="tooltip" translatable="yes">Search</property>
 883                       <property name="can_focus">True</property>
 884                       <property name="label" translatable="yes">search</property>
 885                       <property name="use_underline">True</property>
 886                       <property name="relief">GTK_RELIEF_NORMAL</property>
 887                       <property name="focus_on_click">True</property>
 888                     </widget>
 889                   </child>
 890                 </widget>
 891                 <packing>
 892                   <property name="expand">False</property>
 893                   <property name="homogeneous">False</property>
 894                 </packing>
 895               </child>
 896
 897               <child>
 898                 <widget class="GtkToolItem" id="toolitem19">
 899                   <property name="visible">True</property>
 900                   <property name="visible_horizontal">True</property>
 901                   <property name="visible_vertical">True</property>
 902                   <property name="is_important">False</property>
 903
 904                   <child>
 905                     <widget class="GtkButton" id="autoButton">
 906                       <property name="visible">True</property>
 907                       <property name="tooltip" translatable="yes">Auto</property>
 908                       <property name="can_focus">True</property>
 909                       <property name="label" translatable="yes">auto</property>
 910                       <property name="use_underline">True</property>
 911                       <property name="relief">GTK_RELIEF_NORMAL</property>
 912                       <property name="focus_on_click">True</property>
 913                     </widget>
 914                   </child>
 915                 </widget>
 916                 <packing>
 917                   <property name="expand">False</property>
 918                   <property name="homogeneous">False</property>
 919                 </packing>
 920               </child>
 921             </widget>
 922             <packing>
 923               <property name="padding">0</property>
 924               <property name="expand">False</property>
 925               <property name="fill">False</property>
 926             </packing>
 927           </child>
 928
 929           <child>
 930             <widget class="GtkToolbar" id="toolbar7">
 931               <property name="visible">True</property>
 932               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
 933               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 934               <property name="tooltips">True</property>
 935               <property name="show_arrow">True</property>
 936
 937               <child>
 938                 <widget class="GtkToolItem" id="toolitem20">
 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="cutButton">
 946                       <property name="visible">True</property>
 947                       <property name="tooltip" translatable="yes">Cut</property>
 948                       <property name="can_focus">True</property>
 949                       <property name="label" translatable="yes">cut</property>
 950                       <property name="use_underline">True</property>
 951                       <property name="relief">GTK_RELIEF_NORMAL</property>
 952                       <property name="focus_on_click">True</property>
 953                     </widget>
 954                   </child>
 955                 </widget>
 956                 <packing>
 957                   <property name="expand">False</property>
 958                   <property name="homogeneous">False</property>
 959                 </packing>
 960               </child>
 961
 962               <child>
 963                 <widget class="GtkToolItem" id="toolitem21">
 964                   <property name="visible">True</property>
 965                   <property name="visible_horizontal">True</property>
 966                   <property name="visible_vertical">True</property>
 967                   <property name="is_important">False</property>
 968
 969                   <child>
 970                     <widget class="GtkButton" id="replaceButton">
 971                       <property name="visible">True</property>
 972                       <property name="tooltip" translatable="yes">Replace</property>
 973                       <property name="can_focus">True</property>
 974                       <property name="label" translatable="yes">repl</property>
 975                       <property name="use_underline">True</property>
 976                       <property name="relief">GTK_RELIEF_NORMAL</property>
 977                       <property name="focus_on_click">True</property>
 978                     </widget>
 979                   </child>
 980                 </widget>
 981                 <packing>
 982                   <property name="expand">False</property>
 983                   <property name="homogeneous">False</property>
 984                 </packing>
 985               </child>
 986             </widget>
 987             <packing>
 988               <property name="padding">0</property>
 989               <property name="expand">False</property>
 990               <property name="fill">False</property>
 991             </packing>
 992           </child>
 993         </widget>
 994       </child>
 995     </widget>
 996   </child>
 997 </widget>
 998
 999 <widget class="GtkDialog" id="ConfirmationDialog">
1000   <property name="title" translatable="yes">DUMMY</property>
1001   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1002   <property name="window_position">GTK_WIN_POS_CENTER</property>
1003   <property name="modal">True</property>
1004   <property name="resizable">False</property>
1005   <property name="destroy_with_parent">False</property>
1006   <property name="decorated">True</property>
1007   <property name="skip_taskbar_hint">False</property>
1008   <property name="skip_pager_hint">False</property>
1009   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1010   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1011   <property name="has_separator">True</property>
1012
1013   <child internal-child="vbox">
1014     <widget class="GtkVBox" id="dialog-vbox1">
1015       <property name="visible">True</property>
1016       <property name="homogeneous">False</property>
1017       <property name="spacing">0</property>
1018
1019       <child internal-child="action_area">
1020         <widget class="GtkHButtonBox" id="dialog-action_area1">
1021           <property name="visible">True</property>
1022           <property name="layout_style">GTK_BUTTONBOX_END</property>
1023
1024           <child>
1025             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
1026               <property name="visible">True</property>
1027               <property name="can_default">True</property>
1028               <property name="can_focus">True</property>
1029               <property name="label">gtk-cancel</property>
1030               <property name="use_stock">True</property>
1031               <property name="relief">GTK_RELIEF_NORMAL</property>
1032               <property name="focus_on_click">True</property>
1033               <property name="response_id">-6</property>
1034             </widget>
1035           </child>
1036
1037           <child>
1038             <widget class="GtkButton" id="ConfirmationDialogOkButton">
1039               <property name="visible">True</property>
1040               <property name="can_default">True</property>
1041               <property name="can_focus">True</property>
1042               <property name="label">gtk-ok</property>
1043               <property name="use_stock">True</property>
1044               <property name="relief">GTK_RELIEF_NORMAL</property>
1045               <property name="focus_on_click">True</property>
1046               <property name="response_id">-5</property>
1047             </widget>
1048           </child>
1049         </widget>
1050         <packing>
1051           <property name="padding">0</property>
1052           <property name="expand">False</property>
1053           <property name="fill">True</property>
1054           <property name="pack_type">GTK_PACK_END</property>
1055         </packing>
1056       </child>
1057
1058       <child>
1059         <widget class="GtkLabel" id="ConfirmationDialogLabel">
1060           <property name="visible">True</property>
1061           <property name="label" translatable="yes">DUMMY</property>
1062           <property name="use_underline">False</property>
1063           <property name="use_markup">False</property>
1064           <property name="justify">GTK_JUSTIFY_CENTER</property>
1065           <property name="wrap">False</property>
1066           <property name="selectable">False</property>
1067           <property name="xalign">0.5</property>
1068           <property name="yalign">0.5</property>
1069           <property name="xpad">0</property>
1070           <property name="ypad">0</property>
1071         </widget>
1072         <packing>
1073           <property name="padding">0</property>
1074           <property name="expand">False</property>
1075           <property name="fill">False</property>
1076         </packing>
1077       </child>
1078     </widget>
1079   </child>
1080 </widget>
1081
1082 <widget class="GtkDialog" id="AboutWin">
1083   <property name="title" translatable="yes">Matita: about</property>
1084   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1085   <property name="window_position">GTK_WIN_POS_CENTER</property>
1086   <property name="modal">True</property>
1087   <property name="resizable">False</property>
1088   <property name="destroy_with_parent">False</property>
1089   <property name="decorated">True</property>
1090   <property name="skip_taskbar_hint">False</property>
1091   <property name="skip_pager_hint">False</property>
1092   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1093   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1094   <property name="has_separator">True</property>
1095
1096   <child internal-child="vbox">
1097     <widget class="GtkVBox" id="dialog-vbox2">
1098       <property name="visible">True</property>
1099       <property name="homogeneous">False</property>
1100       <property name="spacing">0</property>
1101
1102       <child internal-child="action_area">
1103         <widget class="GtkHButtonBox" id="dialog-action_area2">
1104           <property name="visible">True</property>
1105           <property name="layout_style">GTK_BUTTONBOX_END</property>
1106
1107           <child>
1108             <widget class="GtkButton" id="AboutDismissButton">
1109               <property name="visible">True</property>
1110               <property name="can_default">True</property>
1111               <property name="can_focus">True</property>
1112               <property name="label">gtk-ok</property>
1113               <property name="use_stock">True</property>
1114               <property name="relief">GTK_RELIEF_NORMAL</property>
1115               <property name="focus_on_click">True</property>
1116               <property name="response_id">-5</property>
1117             </widget>
1118           </child>
1119         </widget>
1120         <packing>
1121           <property name="padding">0</property>
1122           <property name="expand">False</property>
1123           <property name="fill">True</property>
1124           <property name="pack_type">GTK_PACK_END</property>
1125         </packing>
1126       </child>
1127
1128       <child>
1129         <widget class="GtkLabel" id="AboutLabel">
1130           <property name="visible">True</property>
1131           <property name="label" translatable="yes">&lt;b&gt;Matita @VERSION@&lt;/b&gt;
1132
1133 &lt;tt&gt;http://helm.cs.unibo.it&lt;/tt&gt;
1134
1135 Copyright (C) 2004,
1136 &lt;i&gt;the HELM team&lt;/i&gt;</property>
1137           <property name="use_underline">False</property>
1138           <property name="use_markup">True</property>
1139           <property name="justify">GTK_JUSTIFY_CENTER</property>
1140           <property name="wrap">False</property>
1141           <property name="selectable">False</property>
1142           <property name="xalign">0.5</property>
1143           <property name="yalign">0.5</property>
1144           <property name="xpad">5</property>
1145           <property name="ypad">5</property>
1146         </widget>
1147         <packing>
1148           <property name="padding">0</property>
1149           <property name="expand">False</property>
1150           <property name="fill">False</property>
1151         </packing>
1152       </child>
1153     </widget>
1154   </child>
1155 </widget>
1156
1157 <widget class="GtkDialog" id="UriChoiceDialog">
1158   <property name="height_request">280</property>
1159   <property name="title" translatable="yes">Uri choice</property>
1160   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1161   <property name="window_position">GTK_WIN_POS_CENTER</property>
1162   <property name="modal">True</property>
1163   <property name="resizable">True</property>
1164   <property name="destroy_with_parent">False</property>
1165   <property name="decorated">True</property>
1166   <property name="skip_taskbar_hint">False</property>
1167   <property name="skip_pager_hint">False</property>
1168   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1169   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1170   <property name="has_separator">True</property>
1171
1172   <child internal-child="vbox">
1173     <widget class="GtkVBox" id="dialog-vbox3">
1174       <property name="visible">True</property>
1175       <property name="homogeneous">False</property>
1176       <property name="spacing">0</property>
1177
1178       <child internal-child="action_area">
1179         <widget class="GtkHButtonBox" id="dialog-action_area3">
1180           <property name="visible">True</property>
1181           <property name="layout_style">GTK_BUTTONBOX_END</property>
1182
1183           <child>
1184             <widget class="GtkButton" id="UriChoiceAbortButton">
1185               <property name="visible">True</property>
1186               <property name="can_default">True</property>
1187               <property name="can_focus">True</property>
1188               <property name="label">gtk-cancel</property>
1189               <property name="use_stock">True</property>
1190               <property name="relief">GTK_RELIEF_NORMAL</property>
1191               <property name="focus_on_click">True</property>
1192               <property name="response_id">-6</property>
1193             </widget>
1194           </child>
1195
1196           <child>
1197             <widget class="GtkButton" id="UriChoiceSelectedButton">
1198               <property name="visible">True</property>
1199               <property name="can_default">True</property>
1200               <property name="can_focus">True</property>
1201               <property name="relief">GTK_RELIEF_NORMAL</property>
1202               <property name="focus_on_click">True</property>
1203               <property name="response_id">0</property>
1204
1205               <child>
1206                 <widget class="GtkAlignment" id="alignment2">
1207                   <property name="visible">True</property>
1208                   <property name="xalign">0.5</property>
1209                   <property name="yalign">0.5</property>
1210                   <property name="xscale">0</property>
1211                   <property name="yscale">0</property>
1212                   <property name="top_padding">0</property>
1213                   <property name="bottom_padding">0</property>
1214                   <property name="left_padding">0</property>
1215                   <property name="right_padding">0</property>
1216
1217                   <child>
1218                     <widget class="GtkHBox" id="hbox3">
1219                       <property name="visible">True</property>
1220                       <property name="homogeneous">False</property>
1221                       <property name="spacing">2</property>
1222
1223                       <child>
1224                         <widget class="GtkImage" id="image19">
1225                           <property name="visible">True</property>
1226                           <property name="stock">gtk-index</property>
1227                           <property name="icon_size">4</property>
1228                           <property name="xalign">0.5</property>
1229                           <property name="yalign">0.5</property>
1230                           <property name="xpad">0</property>
1231                           <property name="ypad">0</property>
1232                         </widget>
1233                         <packing>
1234                           <property name="padding">0</property>
1235                           <property name="expand">False</property>
1236                           <property name="fill">False</property>
1237                         </packing>
1238                       </child>
1239
1240                       <child>
1241                         <widget class="GtkLabel" id="label3">
1242                           <property name="visible">True</property>
1243                           <property name="label" translatable="yes">Try _Selected</property>
1244                           <property name="use_underline">True</property>
1245                           <property name="use_markup">False</property>
1246                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1247                           <property name="wrap">False</property>
1248                           <property name="selectable">False</property>
1249                           <property name="xalign">0.5</property>
1250                           <property name="yalign">0.5</property>
1251                           <property name="xpad">0</property>
1252                           <property name="ypad">0</property>
1253                         </widget>
1254                         <packing>
1255                           <property name="padding">0</property>
1256                           <property name="expand">False</property>
1257                           <property name="fill">False</property>
1258                         </packing>
1259                       </child>
1260                     </widget>
1261                   </child>
1262                 </widget>
1263               </child>
1264             </widget>
1265           </child>
1266
1267           <child>
1268             <widget class="GtkButton" id="UriChoiceConstantsButton">
1269               <property name="visible">True</property>
1270               <property name="sensitive">False</property>
1271               <property name="can_default">True</property>
1272               <property name="can_focus">True</property>
1273               <property name="label" translatable="yes">Try Constants</property>
1274               <property name="use_underline">True</property>
1275               <property name="relief">GTK_RELIEF_NORMAL</property>
1276               <property name="focus_on_click">True</property>
1277               <property name="response_id">0</property>
1278             </widget>
1279           </child>
1280
1281           <child>
1282             <widget class="GtkButton" id="UriChoiceAutoButton">
1283               <property name="visible">True</property>
1284               <property name="can_default">True</property>
1285               <property name="can_focus">True</property>
1286               <property name="relief">GTK_RELIEF_NORMAL</property>
1287               <property name="focus_on_click">True</property>
1288               <property name="response_id">0</property>
1289
1290               <child>
1291                 <widget class="GtkAlignment" id="alignment1">
1292                   <property name="visible">True</property>
1293                   <property name="xalign">0.5</property>
1294                   <property name="yalign">0.5</property>
1295                   <property name="xscale">0</property>
1296                   <property name="yscale">0</property>
1297                   <property name="top_padding">0</property>
1298                   <property name="bottom_padding">0</property>
1299                   <property name="left_padding">0</property>
1300                   <property name="right_padding">0</property>
1301
1302                   <child>
1303                     <widget class="GtkHBox" id="hbox1">
1304                       <property name="visible">True</property>
1305                       <property name="homogeneous">False</property>
1306                       <property name="spacing">2</property>
1307
1308                       <child>
1309                         <widget class="GtkImage" id="image18">
1310                           <property name="visible">True</property>
1311                           <property name="stock">gtk-ok</property>
1312                           <property name="icon_size">4</property>
1313                           <property name="xalign">0.5</property>
1314                           <property name="yalign">0.5</property>
1315                           <property name="xpad">0</property>
1316                           <property name="ypad">0</property>
1317                         </widget>
1318                         <packing>
1319                           <property name="padding">0</property>
1320                           <property name="expand">False</property>
1321                           <property name="fill">False</property>
1322                         </packing>
1323                       </child>
1324
1325                       <child>
1326                         <widget class="GtkLabel" id="label1">
1327                           <property name="visible">True</property>
1328                           <property name="label" translatable="yes">_Auto</property>
1329                           <property name="use_underline">True</property>
1330                           <property name="use_markup">False</property>
1331                           <property name="justify">GTK_JUSTIFY_LEFT</property>
1332                           <property name="wrap">False</property>
1333                           <property name="selectable">False</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                         <packing>
1340                           <property name="padding">0</property>
1341                           <property name="expand">False</property>
1342                           <property name="fill">False</property>
1343                         </packing>
1344                       </child>
1345                     </widget>
1346                   </child>
1347                 </widget>
1348               </child>
1349             </widget>
1350           </child>
1351         </widget>
1352         <packing>
1353           <property name="padding">0</property>
1354           <property name="expand">False</property>
1355           <property name="fill">True</property>
1356           <property name="pack_type">GTK_PACK_END</property>
1357         </packing>
1358       </child>
1359
1360       <child>
1361         <widget class="GtkVBox" id="vbox2">
1362           <property name="visible">True</property>
1363           <property name="homogeneous">False</property>
1364           <property name="spacing">0</property>
1365
1366           <child>
1367             <widget class="GtkLabel" id="UriChoiceLabel">
1368               <property name="visible">True</property>
1369               <property name="label" translatable="yes">some informative message here ...</property>
1370               <property name="use_underline">False</property>
1371               <property name="use_markup">False</property>
1372               <property name="justify">GTK_JUSTIFY_LEFT</property>
1373               <property name="wrap">False</property>
1374               <property name="selectable">False</property>
1375               <property name="xalign">0.5</property>
1376               <property name="yalign">0.5</property>
1377               <property name="xpad">0</property>
1378               <property name="ypad">0</property>
1379             </widget>
1380             <packing>
1381               <property name="padding">0</property>
1382               <property name="expand">False</property>
1383               <property name="fill">False</property>
1384             </packing>
1385           </child>
1386
1387           <child>
1388             <widget class="GtkScrolledWindow" id="scrolledwindow1">
1389               <property name="visible">True</property>
1390               <property name="can_focus">True</property>
1391               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1392               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1393               <property name="shadow_type">GTK_SHADOW_NONE</property>
1394               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1395
1396               <child>
1397                 <widget class="GtkTreeView" id="UriChoiceTreeView">
1398                   <property name="visible">True</property>
1399                   <property name="can_focus">True</property>
1400                   <property name="headers_visible">False</property>
1401                   <property name="rules_hint">False</property>
1402                   <property name="reorderable">False</property>
1403                   <property name="enable_search">True</property>
1404                 </widget>
1405               </child>
1406             </widget>
1407             <packing>
1408               <property name="padding">0</property>
1409               <property name="expand">True</property>
1410               <property name="fill">True</property>
1411             </packing>
1412           </child>
1413
1414           <child>
1415             <widget class="GtkHBox" id="hbox2">
1416               <property name="visible">True</property>
1417               <property name="homogeneous">False</property>
1418               <property name="spacing">0</property>
1419
1420               <child>
1421                 <widget class="GtkLabel" id="label2">
1422                   <property name="visible">True</property>
1423                   <property name="label" translatable="yes">URI: </property>
1424                   <property name="use_underline">False</property>
1425                   <property name="use_markup">False</property>
1426                   <property name="justify">GTK_JUSTIFY_LEFT</property>
1427                   <property name="wrap">False</property>
1428                   <property name="selectable">False</property>
1429                   <property name="xalign">0.5</property>
1430                   <property name="yalign">0.5</property>
1431                   <property name="xpad">0</property>
1432                   <property name="ypad">0</property>
1433                 </widget>
1434                 <packing>
1435                   <property name="padding">0</property>
1436                   <property name="expand">False</property>
1437                   <property name="fill">False</property>
1438                 </packing>
1439               </child>
1440
1441               <child>
1442                 <widget class="GtkEntry" id="entry1">
1443                   <property name="visible">True</property>
1444                   <property name="can_focus">True</property>
1445                   <property name="editable">True</property>
1446                   <property name="visibility">True</property>
1447                   <property name="max_length">0</property>
1448                   <property name="text" translatable="yes"></property>
1449                   <property name="has_frame">True</property>
1450                   <property name="invisible_char">*</property>
1451                   <property name="activates_default">False</property>
1452                 </widget>
1453                 <packing>
1454                   <property name="padding">0</property>
1455                   <property name="expand">True</property>
1456                   <property name="fill">True</property>
1457                 </packing>
1458               </child>
1459             </widget>
1460             <packing>
1461               <property name="padding">0</property>
1462               <property name="expand">False</property>
1463               <property name="fill">True</property>
1464             </packing>
1465           </child>
1466         </widget>
1467         <packing>
1468           <property name="padding">0</property>
1469           <property name="expand">True</property>
1470           <property name="fill">True</property>
1471         </packing>
1472       </child>
1473     </widget>
1474   </child>
1475 </widget>
1476
1477 <widget class="GtkDialog" id="InterpChoiceDialog">
1478   <property name="height_request">200</property>
1479   <property name="title" translatable="yes">Interpretation choice</property>
1480   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1481   <property name="window_position">GTK_WIN_POS_NONE</property>
1482   <property name="modal">True</property>
1483   <property name="resizable">True</property>
1484   <property name="destroy_with_parent">False</property>
1485   <property name="decorated">True</property>
1486   <property name="skip_taskbar_hint">False</property>
1487   <property name="skip_pager_hint">False</property>
1488   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1489   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1490   <property name="has_separator">True</property>
1491
1492   <child internal-child="vbox">
1493     <widget class="GtkVBox" id="dialog-vbox4">
1494       <property name="visible">True</property>
1495       <property name="homogeneous">False</property>
1496       <property name="spacing">0</property>
1497
1498       <child internal-child="action_area">
1499         <widget class="GtkHButtonBox" id="dialog-action_area4">
1500           <property name="visible">True</property>
1501           <property name="layout_style">GTK_BUTTONBOX_END</property>
1502
1503           <child>
1504             <widget class="GtkButton" id="InterpChoiceHelpButton">
1505               <property name="visible">True</property>
1506               <property name="can_default">True</property>
1507               <property name="can_focus">True</property>
1508               <property name="label">gtk-help</property>
1509               <property name="use_stock">True</property>
1510               <property name="relief">GTK_RELIEF_NORMAL</property>
1511               <property name="focus_on_click">True</property>
1512               <property name="response_id">-11</property>
1513             </widget>
1514           </child>
1515
1516           <child>
1517             <widget class="GtkButton" id="InterpChoiceCancelButton">
1518               <property name="visible">True</property>
1519               <property name="can_default">True</property>
1520               <property name="can_focus">True</property>
1521               <property name="label">gtk-cancel</property>
1522               <property name="use_stock">True</property>
1523               <property name="relief">GTK_RELIEF_NORMAL</property>
1524               <property name="focus_on_click">True</property>
1525               <property name="response_id">-6</property>
1526             </widget>
1527           </child>
1528
1529           <child>
1530             <widget class="GtkButton" id="InterpChoiceOkButton">
1531               <property name="visible">True</property>
1532               <property name="can_default">True</property>
1533               <property name="can_focus">True</property>
1534               <property name="label">gtk-ok</property>
1535               <property name="use_stock">True</property>
1536               <property name="relief">GTK_RELIEF_NORMAL</property>
1537               <property name="focus_on_click">True</property>
1538               <property name="response_id">-5</property>
1539             </widget>
1540           </child>
1541         </widget>
1542         <packing>
1543           <property name="padding">0</property>
1544           <property name="expand">False</property>
1545           <property name="fill">True</property>
1546           <property name="pack_type">GTK_PACK_END</property>
1547         </packing>
1548       </child>
1549
1550       <child>
1551         <widget class="GtkVBox" id="vbox3">
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="InterpChoiceDialogLabel">
1558               <property name="visible">True</property>
1559               <property name="label" translatable="yes">some informative message here ...</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="GtkScrolledWindow" id="scrolledwindow4">
1579               <property name="visible">True</property>
1580               <property name="can_focus">True</property>
1581               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1582               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1583               <property name="shadow_type">GTK_SHADOW_IN</property>
1584               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1585
1586               <child>
1587                 <widget class="GtkTreeView" id="InterpChoiceTreeView">
1588                   <property name="visible">True</property>
1589                   <property name="can_focus">True</property>
1590                   <property name="headers_visible">False</property>
1591                   <property name="rules_hint">False</property>
1592                   <property name="reorderable">False</property>
1593                   <property name="enable_search">True</property>
1594                 </widget>
1595               </child>
1596             </widget>
1597             <packing>
1598               <property name="padding">0</property>
1599               <property name="expand">True</property>
1600               <property name="fill">True</property>
1601             </packing>
1602           </child>
1603         </widget>
1604         <packing>
1605           <property name="padding">0</property>
1606           <property name="expand">True</property>
1607           <property name="fill">True</property>
1608         </packing>
1609       </child>
1610     </widget>
1611   </child>
1612 </widget>
1613
1614 <widget class="GtkDialog" id="EmptyDialog">
1615   <property name="visible">True</property>
1616   <property name="title" translatable="yes">DUMMY</property>
1617   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1618   <property name="window_position">GTK_WIN_POS_NONE</property>
1619   <property name="modal">False</property>
1620   <property name="resizable">True</property>
1621   <property name="destroy_with_parent">False</property>
1622   <property name="decorated">True</property>
1623   <property name="skip_taskbar_hint">False</property>
1624   <property name="skip_pager_hint">False</property>
1625   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
1626   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1627   <property name="has_separator">True</property>
1628
1629   <child internal-child="vbox">
1630     <widget class="GtkVBox" id="EmptyDialogVBox">
1631       <property name="visible">True</property>
1632       <property name="homogeneous">False</property>
1633       <property name="spacing">0</property>
1634
1635       <child internal-child="action_area">
1636         <widget class="GtkHButtonBox" id="dialog-action_area5">
1637           <property name="visible">True</property>
1638           <property name="layout_style">GTK_BUTTONBOX_END</property>
1639
1640           <child>
1641             <widget class="GtkButton" id="EmptyDialogCancelButton">
1642               <property name="visible">True</property>
1643               <property name="can_default">True</property>
1644               <property name="can_focus">True</property>
1645               <property name="label">gtk-cancel</property>
1646               <property name="use_stock">True</property>
1647               <property name="relief">GTK_RELIEF_NORMAL</property>
1648               <property name="focus_on_click">True</property>
1649               <property name="response_id">-6</property>
1650             </widget>
1651           </child>
1652
1653           <child>
1654             <widget class="GtkButton" id="EmptyDialogOkButton">
1655               <property name="visible">True</property>
1656               <property name="can_default">True</property>
1657               <property name="can_focus">True</property>
1658               <property name="label">gtk-ok</property>
1659               <property name="use_stock">True</property>
1660               <property name="relief">GTK_RELIEF_NORMAL</property>
1661               <property name="focus_on_click">True</property>
1662               <property name="response_id">-5</property>
1663             </widget>
1664           </child>
1665         </widget>
1666         <packing>
1667           <property name="padding">0</property>
1668           <property name="expand">False</property>
1669           <property name="fill">True</property>
1670           <property name="pack_type">GTK_PACK_END</property>
1671         </packing>
1672       </child>
1673
1674       <child>
1675         <widget class="GtkLabel" id="EmptyDialogLabel">
1676           <property name="visible">True</property>
1677           <property name="label" translatable="yes">DUMMY</property>
1678           <property name="use_underline">False</property>
1679           <property name="use_markup">False</property>
1680           <property name="justify">GTK_JUSTIFY_LEFT</property>
1681           <property name="wrap">False</property>
1682           <property name="selectable">False</property>
1683           <property name="xalign">0.5</property>
1684           <property name="yalign">0.5</property>
1685           <property name="xpad">0</property>
1686           <property name="ypad">0</property>
1687         </widget>
1688         <packing>
1689           <property name="padding">0</property>
1690           <property name="expand">False</property>
1691           <property name="fill">False</property>
1692         </packing>
1693       </child>
1694
1695       <child>
1696         <placeholder/>
1697       </child>
1698     </widget>
1699   </child>
1700 </widget>
1701
1702 <widget class="GtkWindow" id="CheckWin">
1703   <property name="width_request">300</property>
1704   <property name="height_request">200</property>
1705   <property name="title" translatable="yes">Matita: check term</property>
1706   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1707   <property name="window_position">GTK_WIN_POS_NONE</property>
1708   <property name="modal">False</property>
1709   <property name="resizable">True</property>
1710   <property name="destroy_with_parent">False</property>
1711   <property name="decorated">True</property>
1712   <property name="skip_taskbar_hint">False</property>
1713   <property name="skip_pager_hint">False</property>
1714   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1715   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1716
1717   <child>
1718     <widget class="GtkEventBox" id="CheckWinEventBox">
1719       <property name="visible">True</property>
1720       <property name="visible_window">True</property>
1721       <property name="above_child">False</property>
1722
1723       <child>
1724         <widget class="GtkScrolledWindow" id="ScrolledCheck">
1725           <property name="visible">True</property>
1726           <property name="can_focus">True</property>
1727           <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1728           <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1729           <property name="shadow_type">GTK_SHADOW_NONE</property>
1730           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1731
1732           <child>
1733             <placeholder/>
1734           </child>
1735         </widget>
1736       </child>
1737     </widget>
1738   </child>
1739 </widget>
1740
1741 <widget class="GtkWindow" id="ScriptWin">
1742   <property name="title" translatable="yes">Matita: script</property>
1743   <property name="type">GTK_WINDOW_TOPLEVEL</property>
1744   <property name="window_position">GTK_WIN_POS_NONE</property>
1745   <property name="modal">False</property>
1746   <property name="default_width">450</property>
1747   <property name="default_height">800</property>
1748   <property name="resizable">True</property>
1749   <property name="destroy_with_parent">False</property>
1750   <property name="decorated">True</property>
1751   <property name="skip_taskbar_hint">False</property>
1752   <property name="skip_pager_hint">False</property>
1753   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
1754   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
1755
1756   <child>
1757     <widget class="GtkEventBox" id="ScriptWinEventBox">
1758       <property name="visible">True</property>
1759       <property name="visible_window">True</property>
1760       <property name="above_child">False</property>
1761
1762       <child>
1763         <widget class="GtkNotebook" id="scriptNotebook">
1764           <property name="visible">True</property>
1765           <property name="can_focus">True</property>
1766           <property name="show_tabs">True</property>
1767           <property name="show_border">True</property>
1768           <property name="tab_pos">GTK_POS_BOTTOM</property>
1769           <property name="scrollable">False</property>
1770           <property name="enable_popup">False</property>
1771
1772           <child>
1773             <widget class="GtkVBox" id="vbox4">
1774               <property name="visible">True</property>
1775               <property name="homogeneous">False</property>
1776               <property name="spacing">0</property>
1777
1778               <child>
1779                 <widget class="GtkToolbar" id="toolbar1">
1780                   <property name="visible">True</property>
1781                   <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1782                   <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1783                   <property name="tooltips">True</property>
1784                   <property name="show_arrow">True</property>
1785
1786                   <child>
1787                     <widget class="GtkToolItem" id="toolitem1">
1788                       <property name="visible">True</property>
1789                       <property name="visible_horizontal">True</property>
1790                       <property name="visible_vertical">True</property>
1791                       <property name="is_important">False</property>
1792
1793                       <child>
1794                         <widget class="GtkButton" id="ScriptWinBackButton">
1795                           <property name="visible">True</property>
1796                           <property name="tooltip" translatable="yes">go back 1 phrase</property>
1797                           <property name="can_focus">True</property>
1798                           <property name="relief">GTK_RELIEF_NORMAL</property>
1799                           <property name="focus_on_click">True</property>
1800
1801                           <child>
1802                             <widget class="GtkImage" id="image133">
1803                               <property name="visible">True</property>
1804                               <property name="stock">gtk-go-back</property>
1805                               <property name="icon_size">4</property>
1806                               <property name="xalign">0.5</property>
1807                               <property name="yalign">0.5</property>
1808                               <property name="xpad">0</property>
1809                               <property name="ypad">0</property>
1810                             </widget>
1811                           </child>
1812                         </widget>
1813                       </child>
1814                     </widget>
1815                     <packing>
1816                       <property name="expand">False</property>
1817                       <property name="homogeneous">False</property>
1818                     </packing>
1819                   </child>
1820
1821                   <child>
1822                     <widget class="GtkToolItem" id="toolitem2">
1823                       <property name="visible">True</property>
1824                       <property name="visible_horizontal">True</property>
1825                       <property name="visible_vertical">True</property>
1826                       <property name="is_important">False</property>
1827
1828                       <child>
1829                         <widget class="GtkButton" id="ScriptWinJumpButton">
1830                           <property name="visible">True</property>
1831                           <property name="tooltip" translatable="yes">execute til cursor</property>
1832                           <property name="can_focus">True</property>
1833                           <property name="relief">GTK_RELIEF_NORMAL</property>
1834                           <property name="focus_on_click">True</property>
1835
1836                           <child>
1837                             <widget class="GtkImage" id="image134">
1838                               <property name="visible">True</property>
1839                               <property name="stock">gtk-jump-to</property>
1840                               <property name="icon_size">4</property>
1841                               <property name="xalign">0.5</property>
1842                               <property name="yalign">0.5</property>
1843                               <property name="xpad">0</property>
1844                               <property name="ypad">0</property>
1845                             </widget>
1846                           </child>
1847                         </widget>
1848                       </child>
1849                     </widget>
1850                     <packing>
1851                       <property name="expand">False</property>
1852                       <property name="homogeneous">False</property>
1853                     </packing>
1854                   </child>
1855
1856                   <child>
1857                     <widget class="GtkToolItem" id="toolitem3">
1858                       <property name="visible">True</property>
1859                       <property name="visible_horizontal">True</property>
1860                       <property name="visible_vertical">True</property>
1861                       <property name="is_important">False</property>
1862
1863                       <child>
1864                         <widget class="GtkButton" id="ScriptWinForwardButton">
1865                           <property name="visible">True</property>
1866                           <property name="tooltip" translatable="yes">go forward 1 phrase</property>
1867                           <property name="can_focus">True</property>
1868                           <property name="relief">GTK_RELIEF_NORMAL</property>
1869                           <property name="focus_on_click">True</property>
1870
1871                           <child>
1872                             <widget class="GtkImage" id="image135">
1873                               <property name="visible">True</property>
1874                               <property name="stock">gtk-go-forward</property>
1875                               <property name="icon_size">4</property>
1876                               <property name="xalign">0.5</property>
1877                               <property name="yalign">0.5</property>
1878                               <property name="xpad">0</property>
1879                               <property name="ypad">0</property>
1880                             </widget>
1881                           </child>
1882                         </widget>
1883                       </child>
1884                     </widget>
1885                     <packing>
1886                       <property name="expand">False</property>
1887                       <property name="homogeneous">False</property>
1888                     </packing>
1889                   </child>
1890                 </widget>
1891                 <packing>
1892                   <property name="padding">0</property>
1893                   <property name="expand">False</property>
1894                   <property name="fill">False</property>
1895                 </packing>
1896               </child>
1897
1898               <child>
1899                 <widget class="GtkScrolledWindow" id="ScrolledScript">
1900                   <property name="visible">True</property>
1901                   <property name="can_focus">True</property>
1902                   <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1903                   <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1904                   <property name="shadow_type">GTK_SHADOW_NONE</property>
1905                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1906
1907                   <child>
1908                     <widget class="GtkTextView" id="ScriptTextView">
1909                       <property name="visible">True</property>
1910                       <property name="can_focus">True</property>
1911                       <property name="editable">True</property>
1912                       <property name="overwrite">False</property>
1913                       <property name="accepts_tab">True</property>
1914                       <property name="justification">GTK_JUSTIFY_LEFT</property>
1915                       <property name="wrap_mode">GTK_WRAP_NONE</property>
1916                       <property name="cursor_visible">True</property>
1917                       <property name="pixels_above_lines">0</property>
1918                       <property name="pixels_below_lines">0</property>
1919                       <property name="pixels_inside_wrap">0</property>
1920                       <property name="left_margin">0</property>
1921                       <property name="right_margin">0</property>
1922                       <property name="indent">0</property>
1923                       <property name="text" translatable="yes"></property>
1924                     </widget>
1925                   </child>
1926                 </widget>
1927                 <packing>
1928                   <property name="padding">0</property>
1929                   <property name="expand">True</property>
1930                   <property name="fill">True</property>
1931                 </packing>
1932               </child>
1933             </widget>
1934             <packing>
1935               <property name="tab_expand">False</property>
1936               <property name="tab_fill">True</property>
1937             </packing>
1938           </child>
1939
1940           <child>
1941             <widget class="GtkLabel" id="label7">
1942               <property name="visible">True</property>
1943               <property name="label" translatable="yes">script</property>
1944               <property name="use_underline">False</property>
1945               <property name="use_markup">False</property>
1946               <property name="justify">GTK_JUSTIFY_LEFT</property>
1947               <property name="wrap">False</property>
1948               <property name="selectable">False</property>
1949               <property name="xalign">0.5</property>
1950               <property name="yalign">0.5</property>
1951               <property name="xpad">0</property>
1952               <property name="ypad">0</property>
1953             </widget>
1954             <packing>
1955               <property name="type">tab</property>
1956             </packing>
1957           </child>
1958
1959           <child>
1960             <widget class="GtkScrolledWindow" id="scrolledwindow3">
1961               <property name="visible">True</property>
1962               <property name="can_focus">True</property>
1963               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
1964               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
1965               <property name="shadow_type">GTK_SHADOW_IN</property>
1966               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1967
1968               <child>
1969                 <widget class="GtkTreeView" id="treeview1">
1970                   <property name="visible">True</property>
1971                   <property name="can_focus">True</property>
1972                   <property name="headers_visible">False</property>
1973                   <property name="rules_hint">False</property>
1974                   <property name="reorderable">False</property>
1975                   <property name="enable_search">True</property>
1976                 </widget>
1977               </child>
1978             </widget>
1979             <packing>
1980               <property name="tab_expand">False</property>
1981               <property name="tab_fill">True</property>
1982             </packing>
1983           </child>
1984
1985           <child>
1986             <widget class="GtkLabel" id="label8">
1987               <property name="visible">True</property>
1988               <property name="label" translatable="yes">outline</property>
1989               <property name="use_underline">False</property>
1990               <property name="use_markup">False</property>
1991               <property name="justify">GTK_JUSTIFY_LEFT</property>
1992               <property name="wrap">False</property>
1993               <property name="selectable">False</property>
1994               <property name="xalign">0.5</property>
1995               <property name="yalign">0.5</property>
1996               <property name="xpad">0</property>
1997               <property name="ypad">0</property>
1998             </widget>
1999             <packing>
2000               <property name="type">tab</property>
2001             </packing>
2002           </child>
2003         </widget>
2004       </child>
2005     </widget>
2006   </child>
2007 </widget>
2008
2009 <widget class="GtkDialog" id="TextDialog">
2010   <property name="title" translatable="yes">DUMMY</property>
2011   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2012   <property name="window_position">GTK_WIN_POS_NONE</property>
2013   <property name="modal">False</property>
2014   <property name="resizable">True</property>
2015   <property name="destroy_with_parent">False</property>
2016   <property name="decorated">True</property>
2017   <property name="skip_taskbar_hint">False</property>
2018   <property name="skip_pager_hint">False</property>
2019   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2020   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2021   <property name="has_separator">True</property>
2022
2023   <child internal-child="vbox">
2024     <widget class="GtkVBox" id="vbox5">
2025       <property name="visible">True</property>
2026       <property name="homogeneous">False</property>
2027       <property name="spacing">0</property>
2028
2029       <child internal-child="action_area">
2030         <widget class="GtkHButtonBox" id="hbuttonbox1">
2031           <property name="visible">True</property>
2032           <property name="layout_style">GTK_BUTTONBOX_END</property>
2033
2034           <child>
2035             <widget class="GtkButton" id="TextDialogCancelButton">
2036               <property name="visible">True</property>
2037               <property name="can_default">True</property>
2038               <property name="can_focus">True</property>
2039               <property name="label">gtk-cancel</property>
2040               <property name="use_stock">True</property>
2041               <property name="relief">GTK_RELIEF_NORMAL</property>
2042               <property name="focus_on_click">True</property>
2043               <property name="response_id">-6</property>
2044             </widget>
2045           </child>
2046
2047           <child>
2048             <widget class="GtkButton" id="TextDialogOkButton">
2049               <property name="visible">True</property>
2050               <property name="can_default">True</property>
2051               <property name="can_focus">True</property>
2052               <property name="label">gtk-ok</property>
2053               <property name="use_stock">True</property>
2054               <property name="relief">GTK_RELIEF_NORMAL</property>
2055               <property name="focus_on_click">True</property>
2056               <property name="response_id">-5</property>
2057             </widget>
2058           </child>
2059         </widget>
2060         <packing>
2061           <property name="padding">0</property>
2062           <property name="expand">False</property>
2063           <property name="fill">True</property>
2064           <property name="pack_type">GTK_PACK_END</property>
2065         </packing>
2066       </child>
2067
2068       <child>
2069         <widget class="GtkLabel" id="TextDialogLabel">
2070           <property name="visible">True</property>
2071           <property name="label" translatable="yes">DUMMY</property>
2072           <property name="use_underline">False</property>
2073           <property name="use_markup">False</property>
2074           <property name="justify">GTK_JUSTIFY_LEFT</property>
2075           <property name="wrap">False</property>
2076           <property name="selectable">False</property>
2077           <property name="xalign">0.5</property>
2078           <property name="yalign">0.5</property>
2079           <property name="xpad">0</property>
2080           <property name="ypad">0</property>
2081         </widget>
2082         <packing>
2083           <property name="padding">0</property>
2084           <property name="expand">False</property>
2085           <property name="fill">False</property>
2086         </packing>
2087       </child>
2088
2089       <child>
2090         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2091           <property name="visible">True</property>
2092           <property name="can_focus">True</property>
2093           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2094           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2095           <property name="shadow_type">GTK_SHADOW_IN</property>
2096           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2097
2098           <child>
2099             <widget class="GtkTextView" id="TextDialogTextView">
2100               <property name="visible">True</property>
2101               <property name="can_focus">True</property>
2102               <property name="editable">True</property>
2103               <property name="overwrite">False</property>
2104               <property name="accepts_tab">True</property>
2105               <property name="justification">GTK_JUSTIFY_LEFT</property>
2106               <property name="wrap_mode">GTK_WRAP_NONE</property>
2107               <property name="cursor_visible">True</property>
2108               <property name="pixels_above_lines">0</property>
2109               <property name="pixels_below_lines">0</property>
2110               <property name="pixels_inside_wrap">0</property>
2111               <property name="left_margin">0</property>
2112               <property name="right_margin">0</property>
2113               <property name="indent">0</property>
2114               <property name="text" translatable="yes"></property>
2115             </widget>
2116           </child>
2117         </widget>
2118         <packing>
2119           <property name="padding">0</property>
2120           <property name="expand">True</property>
2121           <property name="fill">True</property>
2122         </packing>
2123       </child>
2124     </widget>
2125   </child>
2126 </widget>
2127
2128 </glade-interface>