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