matita/matita/matita.glade

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE glade-interface SYSTEM "glade-2.0.dtd">
   3 <!--*- mode: xml -*-->
   4 <glade-interface>
   5   <widget class="GtkWindow" id="BrowserWin">
   6     <property name="width_request">500</property>
   7     <property name="height_request">480</property>
   8     <property name="visible">True</property>
   9     <property name="title" translatable="yes">Cic browser</property>
  10     <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
  11     <property name="default_width">500</property>
  12     <property name="default_height">480</property>
  13     <property name="destroy_with_parent">True</property>
  14     <child>
  15       <widget class="GtkEventBox" id="BrowserWinEventBox">
  16         <property name="visible">True</property>
  17         <child>
  18           <widget class="GtkVBox" id="BrowserVBox">
  19             <property name="visible">True</property>
  20             <child>
  21               <widget class="GtkMenuBar" id="menubar2">
  22                 <property name="visible">True</property>
  23                 <child>
  24                   <widget class="GtkMenuItem" id="BrowserFileMenu">
  25                     <property name="visible">True</property>
  26                     <property name="label" translatable="yes">_File</property>
  27                     <property name="use_underline">True</property>
  28                     <child>
  29                       <widget class="GtkMenu" id="BrowserFileMenu_menu">
  30                         <child>
  31                           <widget class="GtkImageMenuItem" id="BrowserNewMenuItem">
  32                             <property name="visible">True</property>
  33                             <property name="label">gtk-new</property>
  34                             <property name="use_underline">True</property>
  35                             <property name="use_stock">True</property>
  36                           </widget>
  37                         </child>
  38                         <child>
  39                           <widget class="GtkMenuItem" id="BrowserUrlMenuItem">
  40                             <property name="visible">True</property>
  41                             <property name="label" translatable="yes">Open _Location ...</property>
  42                             <property name="use_underline">True</property>
  43                             <accelerator key="L" modifiers="GDK_CONTROL_MASK" signal="activate"/>
  44                           </widget>
  45                         </child>
  46                         <child>
  47                           <widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
  48                             <property name="visible">True</property>
  49                           </widget>
  50                         </child>
  51                         <child>
  52                           <widget class="GtkImageMenuItem" id="BrowserCloseMenuItem">
  53                             <property name="visible">True</property>
  54                             <property name="label">gtk-close</property>
  55                             <property name="use_underline">True</property>
  56                             <property name="use_stock">True</property>
  57                           </widget>
  58                         </child>
  59                       </widget>
  60                     </child>
  61                   </widget>
  62                 </child>
  63                 <child>
  64                   <widget class="GtkMenuItem" id="BrowserEditMenu">
  65                     <property name="visible">True</property>
  66                     <property name="label" translatable="yes">_Edit</property>
  67                     <property name="use_underline">True</property>
  68                     <child>
  69                       <widget class="GtkMenu" id="BrowserEditMenu_menu">
  70                         <child>
  71                           <widget class="GtkImageMenuItem" id="BrowserCopyMenuItem">
  72                             <property name="visible">True</property>
  73                             <property name="label">gtk-copy</property>
  74                             <property name="use_underline">True</property>
  75                             <property name="use_stock">True</property>
  76                           </widget>
  77                         </child>
  78                       </widget>
  79                     </child>
  80                   </widget>
  81                 </child>
  82                 <child>
  83                   <widget class="GtkMenuItem" id="BrowserViewMenu">
  84                     <property name="visible">True</property>
  85                     <property name="label" translatable="yes">_View</property>
  86                     <property name="use_underline">True</property>
  87                     <child>
  88                       <widget class="GtkMenu" id="BrowserViewMenu_menu">
  89                         <child>
  90                           <widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
  91                             <property name="visible">True</property>
  92                             <property name="label" translatable="yes">HBugs Tutors</property>
  93                             <property name="use_underline">True</property>
  94                           </widget>
  95                         </child>
  96                       </widget>
  97                     </child>
  98                   </widget>
  99                 </child>
 100               </widget>
 101               <packing>
 102                 <property name="expand">False</property>
 103                 <property name="fill">False</property>
 104               </packing>
 105             </child>
 106             <child>
 107               <widget class="GtkFrame" id="frame2">
 108                 <property name="visible">True</property>
 109                 <property name="label_xalign">0</property>
 110                 <property name="label_yalign">0</property>
 111                 <property name="shadow_type">GTK_SHADOW_NONE</property>
 112                 <child>
 113                   <widget class="GtkHBox" id="BrowserHBox">
 114                     <property name="visible">True</property>
 115                     <child>
 116                       <widget class="GtkButton" id="BrowserNewButton">
 117                         <property name="visible">True</property>
 118                         <property name="can_focus">True</property>
 119                         <property name="relief">GTK_RELIEF_NONE</property>
 120                         <property name="response_id">0</property>
 121                         <child>
 122                           <widget class="GtkImage" id="image303">
 123                             <property name="visible">True</property>
 124                             <property name="stock">gtk-new</property>
 125                           </widget>
 126                         </child>
 127                       </widget>
 128                       <packing>
 129                         <property name="expand">False</property>
 130                         <property name="fill">False</property>
 131                       </packing>
 132                     </child>
 133                     <child>
 134                       <widget class="GtkButton" id="BrowserBackButton">
 135                         <property name="visible">True</property>
 136                         <property name="can_focus">True</property>
 137                         <property name="relief">GTK_RELIEF_NONE</property>
 138                         <property name="response_id">0</property>
 139                         <child>
 140                           <widget class="GtkImage" id="image304">
 141                             <property name="visible">True</property>
 142                             <property name="stock">gtk-go-back</property>
 143                           </widget>
 144                         </child>
 145                       </widget>
 146                       <packing>
 147                         <property name="expand">False</property>
 148                         <property name="fill">False</property>
 149                         <property name="position">1</property>
 150                       </packing>
 151                     </child>
 152                     <child>
 153                       <widget class="GtkButton" id="BrowserForwardButton">
 154                         <property name="visible">True</property>
 155                         <property name="can_focus">True</property>
 156                         <property name="relief">GTK_RELIEF_NONE</property>
 157                         <property name="response_id">0</property>
 158                         <child>
 159                           <widget class="GtkImage" id="image305">
 160                             <property name="visible">True</property>
 161                             <property name="stock">gtk-go-forward</property>
 162                           </widget>
 163                         </child>
 164                       </widget>
 165                       <packing>
 166                         <property name="expand">False</property>
 167                         <property name="fill">False</property>
 168                         <property name="position">2</property>
 169                       </packing>
 170                     </child>
 171                     <child>
 172                       <widget class="GtkButton" id="BrowserRefreshButton">
 173                         <property name="visible">True</property>
 174                         <property name="can_focus">True</property>
 175                         <property name="can_default">True</property>
 176                         <property name="tooltip" translatable="yes">refresh</property>
 177                         <property name="relief">GTK_RELIEF_NONE</property>
 178                         <property name="response_id">0</property>
 179                         <child>
 180                           <widget class="GtkImage" id="image229">
 181                             <property name="visible">True</property>
 182                             <property name="stock">gtk-refresh</property>
 183                           </widget>
 184                         </child>
 185                       </widget>
 186                       <packing>
 187                         <property name="expand">False</property>
 188                         <property name="fill">False</property>
 189                         <property name="position">3</property>
 190                       </packing>
 191                     </child>
 192                     <child>
 193                       <widget class="GtkButton" id="BrowserHomeButton">
 194                         <property name="visible">True</property>
 195                         <property name="can_focus">True</property>
 196                         <property name="can_default">True</property>
 197                         <property name="tooltip" translatable="yes">home</property>
 198                         <property name="relief">GTK_RELIEF_NONE</property>
 199                         <property name="response_id">0</property>
 200                         <child>
 201                           <widget class="GtkImage" id="image190">
 202                             <property name="visible">True</property>
 203                             <property name="stock">gtk-home</property>
 204                           </widget>
 205                         </child>
 206                       </widget>
 207                       <packing>
 208                         <property name="expand">False</property>
 209                         <property name="fill">False</property>
 210                         <property name="position">4</property>
 211                       </packing>
 212                     </child>
 213                     <child>
 214                       <widget class="GtkImage" id="image301">
 215                         <property name="visible">True</property>
 216                         <property name="stock">gtk-jump-to</property>
 217                         <property name="icon_size">2</property>
 218                       </widget>
 219                       <packing>
 220                         <property name="expand">False</property>
 221                         <property name="fill">False</property>
 222                         <property name="padding">3</property>
 223                         <property name="position">5</property>
 224                       </packing>
 225                     </child>
 226                     <child>
 227                       <widget class="GtkHBox" id="UriHBox">
 228                         <property name="visible">True</property>
 229                         <child>
 230                           <placeholder/>
 231                         </child>
 232                       </widget>
 233                       <packing>
 234                         <property name="position">6</property>
 235                       </packing>
 236                     </child>
 237                   </widget>
 238                 </child>
 239               </widget>
 240               <packing>
 241                 <property name="expand">False</property>
 242                 <property name="position">1</property>
 243               </packing>
 244             </child>
 245             <child>
 246               <widget class="GtkNotebook" id="mathOrListNotebook">
 247                 <property name="visible">True</property>
 248                 <property name="can_focus">True</property>
 249                 <child>
 250                   <widget class="GtkScrolledWindow" id="ScrolledBrowser">
 251                     <property name="visible">True</property>
 252                     <property name="can_focus">True</property>
 253                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 254                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 255                     <child>
 256                       <placeholder/>
 257                     </child>
 258                   </widget>
 259                 </child>
 260                 <child>
 261                   <widget class="GtkLabel" id="mathLabel">
 262                     <property name="visible">True</property>
 263                     <property name="label" translatable="yes">MathView</property>
 264                   </widget>
 265                   <packing>
 266                     <property name="type">tab</property>
 267                     <property name="tab_fill">False</property>
 268                   </packing>
 269                 </child>
 270                 <child>
 271                   <widget class="GtkScrolledWindow" id="scrolledwindow9">
 272                     <property name="visible">True</property>
 273                     <property name="can_focus">True</property>
 274                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 275                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 276                     <property name="shadow_type">GTK_SHADOW_IN</property>
 277                     <child>
 278                       <widget class="GtkTreeView" id="whelpResultTreeview">
 279                         <property name="visible">True</property>
 280                         <property name="can_focus">True</property>
 281                         <property name="headers_visible">False</property>
 282                       </widget>
 283                     </child>
 284                   </widget>
 285                   <packing>
 286                     <property name="position">1</property>
 287                   </packing>
 288                 </child>
 289                 <child>
 290                   <widget class="GtkLabel" id="listLabel">
 291                     <property name="visible">True</property>
 292                     <property name="label" translatable="yes">WhelpResults</property>
 293                   </widget>
 294                   <packing>
 295                     <property name="type">tab</property>
 296                     <property name="position">1</property>
 297                     <property name="tab_fill">False</property>
 298                   </packing>
 299                 </child>
 300                 <child>
 301                   <widget class="GtkScrolledWindow" id="scrolledwindow11">
 302                     <property name="visible">True</property>
 303                     <property name="can_focus">True</property>
 304                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 305                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 306                     <child>
 307                       <widget class="GtkViewport" id="viewport2">
 308                         <property name="visible">True</property>
 309                         <property name="shadow_type">GTK_SHADOW_NONE</property>
 310                         <child>
 311                           <widget class="GtkImage" id="BrowserImage">
 312                             <property name="visible">True</property>
 313                             <property name="stock">gtk-missing-image</property>
 314                           </widget>
 315                         </child>
 316                       </widget>
 317                     </child>
 318                   </widget>
 319                   <packing>
 320                     <property name="position">2</property>
 321                   </packing>
 322                 </child>
 323                 <child>
 324                   <widget class="GtkLabel" id="EasterEggLabel">
 325                     <property name="visible">True</property>
 326                     <property name="label" translatable="yes">WhelpEasterEgg</property>
 327                   </widget>
 328                   <packing>
 329                     <property name="type">tab</property>
 330                     <property name="position">2</property>
 331                     <property name="tab_fill">False</property>
 332                   </packing>
 333                 </child>
 334                 <child>
 335                   <widget class="GtkScrolledWindow" id="GraphScrolledWin">
 336                     <property name="visible">True</property>
 337                     <property name="can_focus">True</property>
 338                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 339                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 340                     <child>
 341                       <placeholder/>
 342                     </child>
 343                   </widget>
 344                   <packing>
 345                     <property name="position">3</property>
 346                   </packing>
 347                 </child>
 348                 <child>
 349                   <widget class="GtkLabel" id="label26">
 350                     <property name="visible">True</property>
 351                     <property name="label" translatable="yes">Graph</property>
 352                   </widget>
 353                   <packing>
 354                     <property name="type">tab</property>
 355                     <property name="position">3</property>
 356                     <property name="tab_fill">False</property>
 357                   </packing>
 358                 </child>
 359                 <child>
 360                   <widget class="GtkVBox" id="vbox16">
 361                     <property name="visible">True</property>
 362                     <child>
 363                       <widget class="GtkScrolledWindow" id="scrolledwindow13">
 364                         <property name="visible">True</property>
 365                         <property name="can_focus">True</property>
 366                         <child>
 367                           <widget class="GtkTreeView" id="HBugsTutorsList">
 368                             <property name="visible">True</property>
 369                             <property name="can_focus">True</property>
 370                           </widget>
 371                         </child>
 372                       </widget>
 373                     </child>
 374                     <child>
 375                       <widget class="GtkToolbar" id="toolbar3">
 376                         <property name="visible">True</property>
 377                         <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
 378                         <child>
 379                           <widget class="GtkToolItem" id="toolitem47">
 380                             <property name="visible">True</property>
 381                             <child>
 382                               <widget class="GtkButton" id="HBugsRefreshButton">
 383                                 <property name="visible">True</property>
 384                                 <property name="can_focus">True</property>
 385                                 <property name="label">gtk-refresh</property>
 386                                 <property name="use_stock">True</property>
 387                                 <property name="response_id">0</property>
 388                               </widget>
 389                             </child>
 390                           </widget>
 391                           <packing>
 392                             <property name="expand">False</property>
 393                             <property name="homogeneous">False</property>
 394                           </packing>
 395                         </child>
 396                         <child>
 397                           <widget class="GtkToolItem" id="toolitem48">
 398                             <property name="visible">True</property>
 399                             <child>
 400                               <widget class="GtkButton" id="HBugsUnsubscribeButton">
 401                                 <property name="visible">True</property>
 402                                 <property name="can_focus">True</property>
 403                                 <property name="label">gtk-remove</property>
 404                                 <property name="use_stock">True</property>
 405                                 <property name="response_id">0</property>
 406                               </widget>
 407                             </child>
 408                           </widget>
 409                           <packing>
 410                             <property name="expand">False</property>
 411                             <property name="homogeneous">False</property>
 412                           </packing>
 413                         </child>
 414                         <child>
 415                           <widget class="GtkToolItem" id="toolitem49">
 416                             <property name="visible">True</property>
 417                             <child>
 418                               <widget class="GtkButton" id="HBugsSubscribeButton">
 419                                 <property name="visible">True</property>
 420                                 <property name="can_focus">True</property>
 421                                 <property name="label">gtk-add</property>
 422                                 <property name="use_stock">True</property>
 423                                 <property name="response_id">0</property>
 424                               </widget>
 425                             </child>
 426                           </widget>
 427                           <packing>
 428                             <property name="expand">False</property>
 429                             <property name="homogeneous">False</property>
 430                           </packing>
 431                         </child>
 432                       </widget>
 433                       <packing>
 434                         <property name="expand">False</property>
 435                         <property name="fill">False</property>
 436                         <property name="position">1</property>
 437                       </packing>
 438                     </child>
 439                   </widget>
 440                   <packing>
 441                     <property name="position">4</property>
 442                   </packing>
 443                 </child>
 444                 <child>
 445                   <widget class="GtkLabel" id="label29">
 446                     <property name="visible">True</property>
 447                     <property name="label" translatable="yes">HBugs</property>
 448                   </widget>
 449                   <packing>
 450                     <property name="type">tab</property>
 451                     <property name="position">4</property>
 452                     <property name="tab_fill">False</property>
 453                   </packing>
 454                 </child>
 455                 <child>
 456                   <widget class="GtkScrolledWindow" id="textScrolledWin">
 457                     <property name="visible">True</property>
 458                     <property name="can_focus">True</property>
 459                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 460                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 461                     <child>
 462                       <widget class="GtkTreeView" id="universesTreeview">
 463                         <property name="visible">True</property>
 464                         <property name="can_focus">True</property>
 465                       </widget>
 466                     </child>
 467                   </widget>
 468                   <packing>
 469                     <property name="position">5</property>
 470                   </packing>
 471                 </child>
 472                 <child>
 473                   <widget class="GtkLabel" id="universes">
 474                     <property name="visible">True</property>
 475                     <property name="label" translatable="yes">Universes</property>
 476                   </widget>
 477                   <packing>
 478                     <property name="type">tab</property>
 479                     <property name="position">5</property>
 480                     <property name="tab_fill">False</property>
 481                   </packing>
 482                 </child>
 483                 <child>
 484                   <widget class="GtkVBox" id="vbox20">
 485                     <property name="visible">True</property>
 486                     <child>
 487                       <widget class="GtkScrolledWindow" id="scrolledwinContent">
 488                         <property name="visible">True</property>
 489                         <property name="can_focus">True</property>
 490                         <property name="border_width">3</property>
 491                         <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 492                         <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 493                         <property name="shadow_type">GTK_SHADOW_IN</property>
 494                         <child>
 495                           <placeholder/>
 496                         </child>
 497                       </widget>
 498                     </child>
 499                     <child>
 500                       <widget class="GtkHBox" id="hbox35">
 501                         <property name="visible">True</property>
 502                         <property name="border_width">4</property>
 503                         <property name="spacing">4</property>
 504                         <child>
 505                           <widget class="GtkVBox" id="vbox22">
 506                             <property name="visible">True</property>
 507                             <child>
 508                               <placeholder/>
 509                             </child>
 510                             <child>
 511                               <placeholder/>
 512                             </child>
 513                           </widget>
 514                         </child>
 515                         <child>
 516                           <widget class="GtkEntry" id="entrySearch">
 517                             <property name="visible">True</property>
 518                             <property name="can_focus">True</property>
 519                             <property name="has_focus">True</property>
 520                           </widget>
 521                           <packing>
 522                             <property name="position">1</property>
 523                           </packing>
 524                         </child>
 525                         <child>
 526                           <widget class="GtkButton" id="buttonSearch">
 527                             <property name="visible">True</property>
 528                             <property name="can_focus">True</property>
 529                             <property name="response_id">0</property>
 530                             <child>
 531                               <widget class="GtkAlignment" id="alignment21">
 532                                 <property name="visible">True</property>
 533                                 <property name="xscale">0</property>
 534                                 <property name="yscale">0</property>
 535                                 <child>
 536                                   <widget class="GtkHBox" id="hbox36">
 537                                     <property name="visible">True</property>
 538                                     <property name="spacing">2</property>
 539                                     <child>
 540                                       <widget class="GtkImage" id="image1068">
 541                                         <property name="visible">True</property>
 542                                         <property name="stock">gtk-find</property>
 543                                       </widget>
 544                                       <packing>
 545                                         <property name="expand">False</property>
 546                                         <property name="fill">False</property>
 547                                       </packing>
 548                                     </child>
 549                                     <child>
 550                                       <widget class="GtkLabel" id="label32">
 551                                         <property name="visible">True</property>
 552                                         <property name="label" translatable="yes">Search</property>
 553                                         <property name="use_underline">True</property>
 554                                       </widget>
 555                                       <packing>
 556                                         <property name="expand">False</property>
 557                                         <property name="fill">False</property>
 558                                         <property name="position">1</property>
 559                                       </packing>
 560                                     </child>
 561                                   </widget>
 562                                 </child>
 563                               </widget>
 564                             </child>
 565                           </widget>
 566                           <packing>
 567                             <property name="expand">False</property>
 568                             <property name="fill">False</property>
 569                             <property name="position">2</property>
 570                           </packing>
 571                         </child>
 572                       </widget>
 573                       <packing>
 574                         <property name="expand">False</property>
 575                         <property name="position">1</property>
 576                       </packing>
 577                     </child>
 578                   </widget>
 579                   <packing>
 580                     <property name="position">6</property>
 581                   </packing>
 582                 </child>
 583                 <child>
 584                   <widget class="GtkLabel" id="label1">
 585                     <property name="visible">True</property>
 586                     <property name="label" translatable="yes">SearchText</property>
 587                   </widget>
 588                   <packing>
 589                     <property name="type">tab</property>
 590                     <property name="position">6</property>
 591                     <property name="tab_fill">False</property>
 592                   </packing>
 593                 </child>
 594               </widget>
 595               <packing>
 596                 <property name="position">3</property>
 597               </packing>
 598             </child>
 599           </widget>
 600         </child>
 601       </widget>
 602     </child>
 603   </widget>
 604   <widget class="GtkDialog" id="ConfirmationDialog">
 605     <property name="title" translatable="yes">DUMMY</property>
 606     <property name="resizable">False</property>
 607     <property name="modal">True</property>
 608     <property name="window_position">GTK_WIN_POS_CENTER</property>
 609     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 610     <child internal-child="vbox">
 611       <widget class="GtkVBox" id="dialog-vbox1">
 612         <property name="visible">True</property>
 613         <child>
 614           <widget class="GtkLabel" id="ConfirmationDialogLabel">
 615             <property name="visible">True</property>
 616             <property name="label" translatable="yes">DUMMY</property>
 617             <property name="justify">GTK_JUSTIFY_CENTER</property>
 618           </widget>
 619           <packing>
 620             <property name="expand">False</property>
 621             <property name="fill">False</property>
 622             <property name="position">2</property>
 623           </packing>
 624         </child>
 625         <child internal-child="action_area">
 626           <widget class="GtkHButtonBox" id="dialog-action_area1">
 627             <property name="visible">True</property>
 628             <property name="layout_style">GTK_BUTTONBOX_END</property>
 629             <child>
 630               <widget class="GtkButton" id="ConfirmationDialogCancelButton">
 631                 <property name="visible">True</property>
 632                 <property name="can_focus">True</property>
 633                 <property name="can_default">True</property>
 634                 <property name="label">gtk-cancel</property>
 635                 <property name="use_stock">True</property>
 636                 <property name="response_id">-6</property>
 637               </widget>
 638             </child>
 639             <child>
 640               <widget class="GtkButton" id="ConfirmationDialogOkButton">
 641                 <property name="visible">True</property>
 642                 <property name="can_focus">True</property>
 643                 <property name="can_default">True</property>
 644                 <property name="label">gtk-ok</property>
 645                 <property name="use_stock">True</property>
 646                 <property name="response_id">-5</property>
 647               </widget>
 648               <packing>
 649                 <property name="position">1</property>
 650               </packing>
 651             </child>
 652           </widget>
 653           <packing>
 654             <property name="expand">False</property>
 655             <property name="pack_type">GTK_PACK_END</property>
 656           </packing>
 657         </child>
 658       </widget>
 659     </child>
 660   </widget>
 661   <widget class="GtkDialog" id="EmptyDialog">
 662     <property name="visible">True</property>
 663     <property name="title" translatable="yes">DUMMY</property>
 664     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 665     <child internal-child="vbox">
 666       <widget class="GtkVBox" id="EmptyDialogVBox">
 667         <property name="visible">True</property>
 668         <child>
 669           <widget class="GtkLabel" id="EmptyDialogLabel">
 670             <property name="visible">True</property>
 671             <property name="label" translatable="yes">DUMMY</property>
 672           </widget>
 673           <packing>
 674             <property name="expand">False</property>
 675             <property name="fill">False</property>
 676             <property name="position">2</property>
 677           </packing>
 678         </child>
 679         <child>
 680           <placeholder/>
 681         </child>
 682         <child internal-child="action_area">
 683           <widget class="GtkHButtonBox" id="dialog-action_area5">
 684             <property name="visible">True</property>
 685             <property name="layout_style">GTK_BUTTONBOX_END</property>
 686             <child>
 687               <widget class="GtkButton" id="EmptyDialogCancelButton">
 688                 <property name="visible">True</property>
 689                 <property name="can_focus">True</property>
 690                 <property name="can_default">True</property>
 691                 <property name="label">gtk-cancel</property>
 692                 <property name="use_stock">True</property>
 693                 <property name="response_id">-6</property>
 694               </widget>
 695             </child>
 696             <child>
 697               <widget class="GtkButton" id="EmptyDialogOkButton">
 698                 <property name="visible">True</property>
 699                 <property name="can_focus">True</property>
 700                 <property name="can_default">True</property>
 701                 <property name="label">gtk-ok</property>
 702                 <property name="use_stock">True</property>
 703                 <property name="response_id">-5</property>
 704               </widget>
 705               <packing>
 706                 <property name="position">1</property>
 707               </packing>
 708             </child>
 709           </widget>
 710           <packing>
 711             <property name="expand">False</property>
 712             <property name="pack_type">GTK_PACK_END</property>
 713           </packing>
 714         </child>
 715       </widget>
 716     </child>
 717   </widget>
 718   <widget class="GtkFileSelection" id="FileSelectionWin">
 719     <property name="border_width">10</property>
 720     <property name="title" translatable="yes">Select File</property>
 721     <property name="modal">True</property>
 722     <property name="window_position">GTK_WIN_POS_CENTER</property>
 723     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 724     <property name="show_fileops">True</property>
 725     <child internal-child="cancel_button">
 726       <widget class="GtkButton" id="fileSelCancelButton">
 727         <property name="visible">True</property>
 728         <property name="can_focus">True</property>
 729         <property name="can_default">True</property>
 730         <property name="response_id">0</property>
 731       </widget>
 732     </child>
 733     <child internal-child="ok_button">
 734       <widget class="GtkButton" id="fileSelOkButton">
 735         <property name="visible">True</property>
 736         <property name="can_focus">True</property>
 737         <property name="can_default">True</property>
 738         <property name="response_id">0</property>
 739       </widget>
 740     </child>
 741   </widget>
 742   <widget class="GtkWindow" id="MainWin">
 743     <property name="title" translatable="yes">Matita</property>
 744     <child>
 745       <widget class="GtkEventBox" id="MainWinEventBox">
 746         <property name="visible">True</property>
 747         <child>
 748           <widget class="GtkVBox" id="vbox8">
 749             <property name="visible">True</property>
 750             <child>
 751               <widget class="GtkHandleBox" id="menuBarHandleBox">
 752                 <property name="visible">True</property>
 753                 <property name="shadow_type">GTK_SHADOW_OUT</property>
 754                 <child>
 755                   <widget class="GtkMenuBar" id="menubar1">
 756                     <property name="visible">True</property>
 757                     <child>
 758                       <widget class="GtkMenuItem" id="fileMenu">
 759                         <property name="visible">True</property>
 760                         <property name="label" translatable="yes">_File</property>
 761                         <property name="use_underline">True</property>
 762                         <child>
 763                           <widget class="GtkMenu" id="fileMenu_menu">
 764                             <child>
 765                               <widget class="GtkImageMenuItem" id="newMenuItem">
 766                                 <property name="visible">True</property>
 767                                 <property name="label" translatable="yes">_New</property>
 768                                 <property name="use_underline">True</property>
 769                                 <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 770                                 <child internal-child="image">
 771                                   <widget class="GtkImage" id="image1047">
 772                                     <property name="visible">True</property>
 773                                     <property name="stock">gtk-new</property>
 774                                     <property name="icon_size">1</property>
 775                                   </widget>
 776                                 </child>
 777                               </widget>
 778                             </child>
 779                             <child>
 780                               <widget class="GtkImageMenuItem" id="openMenuItem">
 781                                 <property name="visible">True</property>
 782                                 <property name="label" translatable="yes">_Open...</property>
 783                                 <property name="use_underline">True</property>
 784                                 <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 785                                 <child internal-child="image">
 786                                   <widget class="GtkImage" id="image1048">
 787                                     <property name="visible">True</property>
 788                                     <property name="stock">gtk-open</property>
 789                                     <property name="icon_size">1</property>
 790                                   </widget>
 791                                 </child>
 792                               </widget>
 793                             </child>
 794                             <child>
 795                               <widget class="GtkImageMenuItem" id="saveMenuItem">
 796                                 <property name="visible">True</property>
 797                                 <property name="label" translatable="yes">_Save</property>
 798                                 <property name="use_underline">True</property>
 799                                 <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 800                                 <child internal-child="image">
 801                                   <widget class="GtkImage" id="image1049">
 802                                     <property name="visible">True</property>
 803                                     <property name="stock">gtk-save</property>
 804                                     <property name="icon_size">1</property>
 805                                   </widget>
 806                                 </child>
 807                               </widget>
 808                             </child>
 809                             <child>
 810                               <widget class="GtkImageMenuItem" id="saveAsMenuItem">
 811                                 <property name="visible">True</property>
 812                                 <property name="label" translatable="yes">Save _as ...</property>
 813                                 <property name="use_underline">True</property>
 814                                 <accelerator key="s" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
 815                                 <child internal-child="image">
 816                                   <widget class="GtkImage" id="image1050">
 817                                     <property name="visible">True</property>
 818                                     <property name="stock">gtk-save-as</property>
 819                                     <property name="icon_size">1</property>
 820                                   </widget>
 821                                 </child>
 822                               </widget>
 823                             </child>
 824                             <child>
 825                               <widget class="GtkSeparatorMenuItem" id="separator2">
 826                                 <property name="visible">True</property>
 827                               </widget>
 828                             </child>
 829                             <child>
 830                               <widget class="GtkImageMenuItem" id="quitMenuItem">
 831                                 <property name="visible">True</property>
 832                                 <property name="label" translatable="yes">_Quit</property>
 833                                 <property name="use_underline">True</property>
 834                                 <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 835                                 <child internal-child="image">
 836                                   <widget class="GtkImage" id="image1052">
 837                                     <property name="visible">True</property>
 838                                     <property name="stock">gtk-quit</property>
 839                                     <property name="icon_size">1</property>
 840                                   </widget>
 841                                 </child>
 842                               </widget>
 843                             </child>
 844                           </widget>
 845                         </child>
 846                       </widget>
 847                     </child>
 848                     <child>
 849                       <widget class="GtkMenuItem" id="editMenu">
 850                         <property name="visible">True</property>
 851                         <property name="label" translatable="yes">_Edit</property>
 852                         <property name="use_underline">True</property>
 853                         <child>
 854                           <widget class="GtkMenu" id="editMenu_menu">
 855                             <child>
 856                               <widget class="GtkImageMenuItem" id="undoMenuItem">
 857                                 <property name="visible">True</property>
 858                                 <property name="sensitive">False</property>
 859                                 <property name="label" translatable="yes">_Undo</property>
 860                                 <property name="use_underline">True</property>
 861                                 <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 862                                 <child internal-child="image">
 863                                   <widget class="GtkImage" id="image1053">
 864                                     <property name="visible">True</property>
 865                                     <property name="stock">gtk-undo</property>
 866                                     <property name="icon_size">1</property>
 867                                   </widget>
 868                                 </child>
 869                               </widget>
 870                             </child>
 871                             <child>
 872                               <widget class="GtkImageMenuItem" id="redoMenuItem">
 873                                 <property name="visible">True</property>
 874                                 <property name="sensitive">False</property>
 875                                 <property name="label" translatable="yes">_Redo</property>
 876                                 <property name="use_underline">True</property>
 877                                 <accelerator key="z" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
 878                                 <child internal-child="image">
 879                                   <widget class="GtkImage" id="image1054">
 880                                     <property name="visible">True</property>
 881                                     <property name="stock">gtk-redo</property>
 882                                     <property name="icon_size">1</property>
 883                                   </widget>
 884                                 </child>
 885                               </widget>
 886                             </child>
 887                             <child>
 888                               <widget class="GtkSeparatorMenuItem" id="separator3">
 889                                 <property name="visible">True</property>
 890                               </widget>
 891                             </child>
 892                             <child>
 893                               <widget class="GtkImageMenuItem" id="cutMenuItem">
 894                                 <property name="visible">True</property>
 895                                 <property name="label" translatable="yes">Cu_t</property>
 896                                 <property name="use_underline">True</property>
 897                                 <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 898                                 <child internal-child="image">
 899                                   <widget class="GtkImage" id="image1055">
 900                                     <property name="visible">True</property>
 901                                     <property name="stock">gtk-cut</property>
 902                                     <property name="icon_size">1</property>
 903                                   </widget>
 904                                 </child>
 905                               </widget>
 906                             </child>
 907                             <child>
 908                               <widget class="GtkImageMenuItem" id="copyMenuItem">
 909                                 <property name="visible">True</property>
 910                                 <property name="label" translatable="yes">_Copy</property>
 911                                 <property name="use_underline">True</property>
 912                                 <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 913                                 <child internal-child="image">
 914                                   <widget class="GtkImage" id="image1056">
 915                                     <property name="visible">True</property>
 916                                     <property name="stock">gtk-copy</property>
 917                                     <property name="icon_size">1</property>
 918                                   </widget>
 919                                 </child>
 920                               </widget>
 921                             </child>
 922                             <child>
 923                               <widget class="GtkImageMenuItem" id="pasteMenuItem">
 924                                 <property name="visible">True</property>
 925                                 <property name="label" translatable="yes">_Paste</property>
 926                                 <property name="use_underline">True</property>
 927                                 <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 928                                 <child internal-child="image">
 929                                   <widget class="GtkImage" id="image1057">
 930                                     <property name="visible">True</property>
 931                                     <property name="stock">gtk-paste</property>
 932                                     <property name="icon_size">1</property>
 933                                   </widget>
 934                                 </child>
 935                               </widget>
 936                             </child>
 937                             <child>
 938                               <widget class="GtkMenuItem" id="pastePatternMenuItem">
 939                                 <property name="visible">True</property>
 940                                 <property name="label" translatable="yes">Paste as pattern</property>
 941                                 <property name="use_underline">True</property>
 942                               </widget>
 943                             </child>
 944                             <child>
 945                               <widget class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
 946                                 <property name="visible">True</property>
 947                                 <property name="label" translatable="yes">Paste Unicode as TeX</property>
 948                                 <property name="use_underline">True</property>
 949                               </widget>
 950                             </child>
 951                             <child>
 952                               <widget class="GtkCheckMenuItem" id="menuitemAutoAltL">
 953                                 <property name="visible">True</property>
 954                                 <property name="tooltip" translatable="yes">Automatically expands TeX macros to their corresponding UTF-8 symbol</property>
 955                                 <property name="label" translatable="yes">Auto-expand TeX Macros</property>
 956                                 <property name="use_underline">True</property>
 957                                 <property name="active">True</property>
 958                               </widget>
 959                             </child>
 960                             <child>
 961                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
 962                                 <property name="visible">True</property>
 963                                 <property name="label" translatable="yes">_Delete</property>
 964                                 <property name="use_underline">True</property>
 965                                 <child internal-child="image">
 966                                   <widget class="GtkImage" id="image1058">
 967                                     <property name="visible">True</property>
 968                                     <property name="stock">gtk-delete</property>
 969                                     <property name="icon_size">1</property>
 970                                   </widget>
 971                                 </child>
 972                               </widget>
 973                             </child>
 974                             <child>
 975                               <widget class="GtkSeparatorMenuItem" id="separator4">
 976                                 <property name="visible">True</property>
 977                               </widget>
 978                             </child>
 979                             <child>
 980                               <widget class="GtkMenuItem" id="selectAllMenuItem">
 981                                 <property name="visible">True</property>
 982                                 <property name="label" translatable="yes">Select _All</property>
 983                                 <property name="use_underline">True</property>
 984                               </widget>
 985                             </child>
 986                             <child>
 987                               <widget class="GtkSeparatorMenuItem" id="separator7">
 988                                 <property name="visible">True</property>
 989                               </widget>
 990                             </child>
 991                             <child>
 992                               <widget class="GtkImageMenuItem" id="findReplMenuItem">
 993                                 <property name="visible">True</property>
 994                                 <property name="label" translatable="yes">_Find &amp; replace ...</property>
 995                                 <property name="use_underline">True</property>
 996                                 <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 997                                 <child internal-child="image">
 998                                   <widget class="GtkImage" id="image1059">
 999                                     <property name="visible">True</property>
1000                                     <property name="stock">gtk-find-and-replace</property>
1001                                     <property name="icon_size">1</property>
1002                                   </widget>
1003                                 </child>
1004                               </widget>
1005                             </child>
1006                             <child>
1007                               <widget class="GtkSeparatorMenuItem" id="separator8">
1008                                 <property name="visible">True</property>
1009                               </widget>
1010                             </child>
1011                             <child>
1012                               <widget class="GtkMenuItem" id="LigatureButton">
1013                                 <property name="visible">True</property>
1014                                 <property name="label" translatable="yes">Next ligature</property>
1015                                 <property name="use_underline">True</property>
1016                                 <accelerator key="l" modifiers="GDK_MOD1_MASK" signal="activate"/>
1017                               </widget>
1018                             </child>
1019                             <child>
1020                               <widget class="GtkMenuItem" id="externalEditorMenuItem">
1021                                 <property name="visible">True</property>
1022                                 <property name="label" translatable="yes">Edit with e_xternal editor</property>
1023                                 <property name="use_underline">True</property>
1024                               </widget>
1025                             </child>
1026                           </widget>
1027                         </child>
1028                       </widget>
1029                     </child>
1030                     <child>
1031                       <widget class="GtkMenuItem" id="scriptMenu">
1032                         <property name="visible">True</property>
1033                         <property name="label" translatable="yes">_Script</property>
1034                         <property name="use_underline">True</property>
1035                         <child>
1036                           <widget class="GtkMenu" id="scriptMenu_menu">
1037                             <child>
1038                               <widget class="GtkMenuItem" id="scriptAdvanceMenuItem">
1039                                 <property name="visible">True</property>
1040                                 <property name="label" translatable="yes">Execute 1 phrase</property>
1041                                 <property name="use_underline">True</property>
1042                                 <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1043                               </widget>
1044                             </child>
1045                             <child>
1046                               <widget class="GtkMenuItem" id="scriptRetractMenuItem">
1047                                 <property name="visible">True</property>
1048                                 <property name="label" translatable="yes">Retract 1 phrase</property>
1049                                 <property name="use_underline">True</property>
1050                                 <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1051                               </widget>
1052                             </child>
1053                             <child>
1054                               <widget class="GtkSeparatorMenuItem" id="separator9">
1055                                 <property name="visible">True</property>
1056                               </widget>
1057                             </child>
1058                             <child>
1059                               <widget class="GtkMenuItem" id="scriptBottomMenuItem">
1060                                 <property name="visible">True</property>
1061                                 <property name="label" translatable="yes">Execute all</property>
1062                                 <property name="use_underline">True</property>
1063                                 <accelerator key="End" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1064                               </widget>
1065                             </child>
1066                             <child>
1067                               <widget class="GtkMenuItem" id="scriptTopMenuItem">
1068                                 <property name="visible">True</property>
1069                                 <property name="label" translatable="yes">Restart</property>
1070                                 <property name="use_underline">True</property>
1071                                 <accelerator key="Home" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1072                               </widget>
1073                             </child>
1074                             <child>
1075                               <widget class="GtkSeparatorMenuItem" id="separator10">
1076                                 <property name="visible">True</property>
1077                               </widget>
1078                             </child>
1079                             <child>
1080                               <widget class="GtkMenuItem" id="scriptJumpMenuItem">
1081                                 <property name="visible">True</property>
1082                                 <property name="label" translatable="yes">Execute until cursor</property>
1083                                 <property name="use_underline">True</property>
1084                                 <accelerator key="period" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1085                               </widget>
1086                             </child>
1087                           </widget>
1088                         </child>
1089                       </widget>
1090                     </child>
1091                     <child>
1092                       <widget class="GtkMenuItem" id="viewMenu">
1093                         <property name="visible">True</property>
1094                         <property name="label" translatable="yes">_View</property>
1095                         <property name="use_underline">True</property>
1096                         <child>
1097                           <widget class="GtkMenu" id="viewMenu_menu">
1098                             <child>
1099                               <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1100                                 <property name="visible">True</property>
1101                                 <property name="label" translatable="yes">New CIC _browser</property>
1102                                 <property name="use_underline">True</property>
1103                                 <accelerator key="F3" modifiers="" signal="activate"/>
1104                               </widget>
1105                             </child>
1106                             <child>
1107                               <widget class="GtkSeparatorMenuItem" id="separator5">
1108                                 <property name="visible">True</property>
1109                               </widget>
1110                             </child>
1111                             <child>
1112                               <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1113                                 <property name="visible">True</property>
1114                                 <property name="label" translatable="yes">_Fullscreen</property>
1115                                 <property name="use_underline">True</property>
1116                                 <accelerator key="F11" modifiers="" signal="activate"/>
1117                               </widget>
1118                             </child>
1119                             <child>
1120                               <widget class="GtkCheckMenuItem" id="menuitemPalette">
1121                                 <property name="visible">True</property>
1122                                 <property name="tooltip" translatable="yes">Shows a palette with natural deduction rules</property>
1123                                 <property name="label" translatable="yes">Natural deduction palette</property>
1124                                 <property name="use_underline">True</property>
1125                                 <accelerator key="F2" modifiers="" signal="activate"/>
1126                               </widget>
1127                             </child>
1128                             <child>
1129                               <widget class="GtkSeparatorMenuItem" id="separator1">
1130                                 <property name="visible">True</property>
1131                               </widget>
1132                             </child>
1133                             <child>
1134                               <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
1135                                 <property name="visible">True</property>
1136                                 <property name="label" translatable="yes">Zoom _in</property>
1137                                 <property name="use_underline">True</property>
1138                                 <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1139                                 <child internal-child="image">
1140                                   <widget class="GtkImage" id="image1060">
1141                                     <property name="visible">True</property>
1142                                     <property name="stock">gtk-zoom-in</property>
1143                                     <property name="icon_size">1</property>
1144                                   </widget>
1145                                 </child>
1146                               </widget>
1147                             </child>
1148                             <child>
1149                               <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
1150                                 <property name="visible">True</property>
1151                                 <property name="label" translatable="yes">Zoom _out</property>
1152                                 <property name="use_underline">True</property>
1153                                 <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1154                                 <child internal-child="image">
1155                                   <widget class="GtkImage" id="image1061">
1156                                     <property name="visible">True</property>
1157                                     <property name="stock">gtk-zoom-out</property>
1158                                     <property name="icon_size">1</property>
1159                                   </widget>
1160                                 </child>
1161                               </widget>
1162                             </child>
1163                             <child>
1164                               <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
1165                                 <property name="visible">True</property>
1166                                 <property name="label" translatable="yes">_Normal size</property>
1167                                 <property name="use_underline">True</property>
1168                                 <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1169                                 <child internal-child="image">
1170                                   <widget class="GtkImage" id="image1062">
1171                                     <property name="visible">True</property>
1172                                     <property name="stock">gtk-zoom-100</property>
1173                                     <property name="icon_size">1</property>
1174                                   </widget>
1175                                 </child>
1176                               </widget>
1177                             </child>
1178                             <child>
1179                               <widget class="GtkSeparatorMenuItem" id="separator12">
1180                                 <property name="visible">True</property>
1181                               </widget>
1182                             </child>
1183                             <child>
1184                               <widget class="GtkCheckMenuItem" id="ppNotationMenuItem">
1185                                 <property name="visible">True</property>
1186                                 <property name="label" translatable="yes">Pretty print notation</property>
1187                                 <property name="use_underline">True</property>
1188                                 <property name="active">True</property>
1189                               </widget>
1190                             </child>
1191                             <child>
1192                               <widget class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
1193                                 <property name="visible">True</property>
1194                                 <property name="label" translatable="yes">Hide coercions</property>
1195                                 <property name="use_underline">True</property>
1196                                 <property name="active">True</property>
1197                               </widget>
1198                             </child>
1199                             <child>
1200                               <widget class="GtkSeparatorMenuItem" id="separator13">
1201                                 <property name="visible">True</property>
1202                               </widget>
1203                             </child>
1204                             <child>
1205                               <widget class="GtkMenuItem" id="showCoercionsGraphMenuItem">
1206                                 <property name="visible">True</property>
1207                                 <property name="tooltip" translatable="yes">Displays the graph of coercions</property>
1208                                 <property name="label" translatable="yes">Coercions Graph</property>
1209                                 <property name="use_underline">True</property>
1210                               </widget>
1211                             </child>
1212                             <child>
1213                               <widget class="GtkMenuItem" id="showHintsDbMenuItem">
1214                                 <property name="visible">True</property>
1215                                 <property name="tooltip" translatable="yes">Displays the database of hints</property>
1216                                 <property name="label" translatable="yes">Hints database</property>
1217                                 <property name="use_underline">True</property>
1218                               </widget>
1219                             </child>
1220                             <child>
1221                               <widget class="GtkMenuItem" id="showTermGrammarMenuItem">
1222                                 <property name="visible">True</property>
1223                                 <property name="tooltip" translatable="yes">Displays the terms grammar as extended by the user</property>
1224                                 <property name="label" translatable="yes">Terms grammar</property>
1225                                 <property name="use_underline">True</property>
1226                               </widget>
1227                             </child>
1228                             <child>
1229                               <widget class="GtkImageMenuItem" id="showUnicodeTable">
1230                                 <property name="visible">True</property>
1231                                 <property name="tooltip" translatable="yes">Show the conversion table from TeX like sequences to UTF-8</property>
1232                                 <property name="label" translatable="yes">TeX/UTF-8 table</property>
1233                                 <property name="use_underline">True</property>
1234                                 <child internal-child="image">
1235                                   <widget class="GtkImage" id="menu-item-image20">
1236                                     <property name="visible">True</property>
1237                                     <property name="stock">gtk-select-font</property>
1238                                   </widget>
1239                                 </child>
1240                               </widget>
1241                             </child>
1242                           </widget>
1243                         </child>
1244                       </widget>
1245                     </child>
1246                     <child>
1247                       <widget class="GtkMenuItem" id="debugMenu">
1248                         <property name="visible">True</property>
1249                         <property name="label" translatable="yes">_Debug</property>
1250                         <property name="use_underline">True</property>
1251                         <child>
1252                           <widget class="GtkMenu" id="debugMenu_menu">
1253                             <child>
1254                               <widget class="GtkSeparatorMenuItem" id="separator6">
1255                                 <property name="visible">True</property>
1256                               </widget>
1257                             </child>
1258                           </widget>
1259                         </child>
1260                       </widget>
1261                     </child>
1262                     <child>
1263                       <widget class="GtkMenuItem" id="helpMenu">
1264                         <property name="visible">True</property>
1265                         <property name="label" translatable="yes">_Help</property>
1266                         <property name="use_underline">True</property>
1267                         <child>
1268                           <widget class="GtkMenu" id="helpMenu_menu">
1269                             <child>
1270                               <widget class="GtkImageMenuItem" id="contentsMenuItem">
1271                                 <property name="visible">True</property>
1272                                 <property name="label" translatable="yes">_Contents</property>
1273                                 <property name="use_underline">True</property>
1274                                 <accelerator key="F1" modifiers="" signal="activate"/>
1275                                 <child internal-child="image">
1276                                   <widget class="GtkImage" id="image1063">
1277                                     <property name="visible">True</property>
1278                                     <property name="stock">gtk-help</property>
1279                                     <property name="icon_size">1</property>
1280                                   </widget>
1281                                 </child>
1282                               </widget>
1283                             </child>
1284                             <child>
1285                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
1286                                 <property name="visible">True</property>
1287                                 <property name="label" translatable="yes">_About</property>
1288                                 <property name="use_underline">True</property>
1289                                 <child internal-child="image">
1290                                   <widget class="GtkImage" id="image1064">
1291                                     <property name="visible">True</property>
1292                                     <property name="stock">gtk-about</property>
1293                                     <property name="icon_size">1</property>
1294                                   </widget>
1295                                 </child>
1296                               </widget>
1297                             </child>
1298                           </widget>
1299                         </child>
1300                       </widget>
1301                     </child>
1302                   </widget>
1303                 </child>
1304               </widget>
1305               <packing>
1306                 <property name="expand">False</property>
1307                 <property name="fill">False</property>
1308               </packing>
1309             </child>
1310             <child>
1311               <widget class="GtkHBox" id="hbox99">
1312                 <property name="visible">True</property>
1313                 <child>
1314                   <widget class="GtkHPaned" id="hpaneScriptSequent">
1315                     <property name="visible">True</property>
1316                     <property name="can_focus">True</property>
1317                     <child>
1318                       <widget class="GtkHBox" id="hbox18">
1319                         <property name="visible">True</property>
1320                         <property name="spacing">2</property>
1321                         <child>
1322                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1323                             <property name="visible">True</property>
1324                             <property name="shadow_type">GTK_SHADOW_OUT</property>
1325                             <property name="handle_position">GTK_POS_TOP</property>
1326                             <child>
1327                               <widget class="GtkVBox" id="vboxTacticsPalette">
1328                                 <property name="visible">True</property>
1329                                 <child>
1330                                   <widget class="GtkExpander" id="expander1">
1331                                     <property name="visible">True</property>
1332                                     <property name="can_focus">True</property>
1333                                     <child>
1334                                       <widget class="GtkVBox" id="vbox1">
1335                                         <property name="visible">True</property>
1336                                         <child>
1337                                           <widget class="GtkButton" id="butImpl_intro">
1338                                             <property name="visible">True</property>
1339                                             <property name="can_focus">True</property>
1340                                             <property name="receives_default">True</property>
1341                                             <property name="response_id">0</property>
1342                                             <child>
1343                                               <widget class="GtkLabel" id="label8">
1344                                                 <property name="visible">True</property>
1345                                                 <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;i&lt;/sub&gt;)</property>
1346                                                 <property name="use_markup">True</property>
1347                                               </widget>
1348                                             </child>
1349                                           </widget>
1350                                         </child>
1351                                         <child>
1352                                           <widget class="GtkButton" id="butAnd_intro">
1353                                             <property name="visible">True</property>
1354                                             <property name="can_focus">True</property>
1355                                             <property name="receives_default">True</property>
1356                                             <property name="response_id">0</property>
1357                                             <child>
1358                                               <widget class="GtkLabel" id="label7">
1359                                                 <property name="visible">True</property>
1360                                                 <property name="label" translatable="yes">Conjunction (∧&lt;sub&gt;i&lt;/sub&gt;)</property>
1361                                                 <property name="use_markup">True</property>
1362                                               </widget>
1363                                             </child>
1364                                           </widget>
1365                                           <packing>
1366                                             <property name="position">1</property>
1367                                           </packing>
1368                                         </child>
1369                                         <child>
1370                                           <widget class="GtkButton" id="butOr_intro_left">
1371                                             <property name="visible">True</property>
1372                                             <property name="can_focus">True</property>
1373                                             <property name="receives_default">True</property>
1374                                             <property name="response_id">0</property>
1375                                             <child>
1376                                               <widget class="GtkLabel" id="label9">
1377                                                 <property name="visible">True</property>
1378                                                 <property name="label" translatable="yes">Disjunction left (∨&lt;sub&gt;i-l&lt;/sub&gt;)</property>
1379                                                 <property name="use_markup">True</property>
1380                                               </widget>
1381                                             </child>
1382                                           </widget>
1383                                           <packing>
1384                                             <property name="position">2</property>
1385                                           </packing>
1386                                         </child>
1387                                         <child>
1388                                           <widget class="GtkButton" id="butOr_intro_right">
1389                                             <property name="visible">True</property>
1390                                             <property name="can_focus">True</property>
1391                                             <property name="receives_default">True</property>
1392                                             <property name="response_id">0</property>
1393                                             <child>
1394                                               <widget class="GtkLabel" id="label10">
1395                                                 <property name="visible">True</property>
1396                                                 <property name="label" translatable="yes">Disjunction right (∨&lt;sub&gt;i-r&lt;/sub&gt;)</property>
1397                                                 <property name="use_markup">True</property>
1398                                               </widget>
1399                                             </child>
1400                                           </widget>
1401                                           <packing>
1402                                             <property name="position">3</property>
1403                                           </packing>
1404                                         </child>
1405                                         <child>
1406                                           <widget class="GtkButton" id="butNot_intro">
1407                                             <property name="visible">True</property>
1408                                             <property name="can_focus">True</property>
1409                                             <property name="receives_default">True</property>
1410                                             <property name="response_id">0</property>
1411                                             <child>
1412                                               <widget class="GtkLabel" id="label11">
1413                                                 <property name="visible">True</property>
1414                                                 <property name="label" translatable="yes">Negation (¬&lt;sub&gt;i&lt;/sub&gt;)</property>
1415                                                 <property name="use_markup">True</property>
1416                                               </widget>
1417                                             </child>
1418                                           </widget>
1419                                           <packing>
1420                                             <property name="position">4</property>
1421                                           </packing>
1422                                         </child>
1423                                         <child>
1424                                           <widget class="GtkButton" id="butTop_intro">
1425                                             <property name="visible">True</property>
1426                                             <property name="can_focus">True</property>
1427                                             <property name="receives_default">True</property>
1428                                             <property name="response_id">0</property>
1429                                             <child>
1430                                               <widget class="GtkLabel" id="label12">
1431                                                 <property name="visible">True</property>
1432                                                 <property name="label" translatable="yes">Top (⊤&lt;sub&gt;i&lt;/sub&gt;)</property>
1433                                                 <property name="use_markup">True</property>
1434                                               </widget>
1435                                             </child>
1436                                           </widget>
1437                                           <packing>
1438                                             <property name="position">5</property>
1439                                           </packing>
1440                                         </child>
1441                                         <child>
1442                                           <widget class="GtkButton" id="butForall_intro">
1443                                             <property name="visible">True</property>
1444                                             <property name="can_focus">True</property>
1445                                             <property name="receives_default">True</property>
1446                                             <property name="response_id">0</property>
1447                                             <child>
1448                                               <widget class="GtkLabel" id="label20">
1449                                                 <property name="visible">True</property>
1450                                                 <property name="label" translatable="yes">Universal (∀&lt;sub&gt;i&lt;/sub&gt;)</property>
1451                                                 <property name="use_markup">True</property>
1452                                               </widget>
1453                                             </child>
1454                                           </widget>
1455                                           <packing>
1456                                             <property name="position">6</property>
1457                                           </packing>
1458                                         </child>
1459                                         <child>
1460                                           <widget class="GtkButton" id="butExists_intro">
1461                                             <property name="visible">True</property>
1462                                             <property name="can_focus">True</property>
1463                                             <property name="receives_default">True</property>
1464                                             <property name="response_id">0</property>
1465                                             <child>
1466                                               <widget class="GtkLabel" id="label21">
1467                                                 <property name="visible">True</property>
1468                                                 <property name="label" translatable="yes">Existential (∃&lt;sub&gt;i&lt;/sub&gt;)</property>
1469                                                 <property name="use_markup">True</property>
1470                                               </widget>
1471                                             </child>
1472                                           </widget>
1473                                           <packing>
1474                                             <property name="position">7</property>
1475                                           </packing>
1476                                         </child>
1477                                       </widget>
1478                                     </child>
1479                                     <child>
1480                                       <widget class="GtkLabel" id="label4">
1481                                         <property name="visible">True</property>
1482                                         <property name="label" translatable="yes">Introduction rules</property>
1483                                       </widget>
1484                                       <packing>
1485                                         <property name="type">label_item</property>
1486                                       </packing>
1487                                     </child>
1488                                   </widget>
1489                                   <packing>
1490                                     <property name="expand">False</property>
1491                                   </packing>
1492                                 </child>
1493                                 <child>
1494                                   <widget class="GtkExpander" id="expander2">
1495                                     <property name="visible">True</property>
1496                                     <property name="can_focus">True</property>
1497                                     <child>
1498                                       <widget class="GtkVBox" id="vbox3">
1499                                         <property name="visible">True</property>
1500                                         <child>
1501                                           <widget class="GtkButton" id="butImpl_elim">
1502                                             <property name="visible">True</property>
1503                                             <property name="can_focus">True</property>
1504                                             <property name="receives_default">True</property>
1505                                             <property name="response_id">0</property>
1506                                             <child>
1507                                               <widget class="GtkLabel" id="label22">
1508                                                 <property name="visible">True</property>
1509                                                 <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;e&lt;/sub&gt;)</property>
1510                                                 <property name="use_markup">True</property>
1511                                               </widget>
1512                                             </child>
1513                                           </widget>
1514                                         </child>
1515                                         <child>
1516                                           <widget class="GtkButton" id="butAnd_elim_left">
1517                                             <property name="visible">True</property>
1518                                             <property name="can_focus">True</property>
1519                                             <property name="receives_default">True</property>
1520                                             <property name="response_id">0</property>
1521                                             <child>
1522                                               <widget class="GtkLabel" id="label23">
1523                                                 <property name="visible">True</property>
1524                                                 <property name="label" translatable="yes">Conjunction left (∧&lt;sub&gt;e-l&lt;/sub&gt;)</property>
1525                                                 <property name="use_markup">True</property>
1526                                               </widget>
1527                                             </child>
1528                                           </widget>
1529                                           <packing>
1530                                             <property name="position">1</property>
1531                                           </packing>
1532                                         </child>
1533                                         <child>
1534                                           <widget class="GtkButton" id="butAnd_elim_right">
1535                                             <property name="visible">True</property>
1536                                             <property name="can_focus">True</property>
1537                                             <property name="receives_default">True</property>
1538                                             <property name="response_id">0</property>
1539                                             <child>
1540                                               <widget class="GtkLabel" id="label24">
1541                                                 <property name="visible">True</property>
1542                                                 <property name="label" translatable="yes">Conjunction right (∧&lt;sub&gt;e-r&lt;/sub&gt;)</property>
1543                                                 <property name="use_markup">True</property>
1544                                               </widget>
1545                                             </child>
1546                                           </widget>
1547                                           <packing>
1548                                             <property name="position">2</property>
1549                                           </packing>
1550                                         </child>
1551                                         <child>
1552                                           <widget class="GtkButton" id="butOr_elim">
1553                                             <property name="visible">True</property>
1554                                             <property name="can_focus">True</property>
1555                                             <property name="receives_default">True</property>
1556                                             <property name="response_id">0</property>
1557                                             <child>
1558                                               <widget class="GtkLabel" id="label27">
1559                                                 <property name="visible">True</property>
1560                                                 <property name="label" translatable="yes">Disjunction (∨&lt;sub&gt;e&lt;/sub&gt;)</property>
1561                                                 <property name="use_markup">True</property>
1562                                               </widget>
1563                                             </child>
1564                                           </widget>
1565                                           <packing>
1566                                             <property name="position">3</property>
1567                                           </packing>
1568                                         </child>
1569                                         <child>
1570                                           <widget class="GtkButton" id="butNot_elim">
1571                                             <property name="visible">True</property>
1572                                             <property name="can_focus">True</property>
1573                                             <property name="receives_default">True</property>
1574                                             <property name="response_id">0</property>
1575                                             <child>
1576                                               <widget class="GtkLabel" id="label31">
1577                                                 <property name="visible">True</property>
1578                                                 <property name="label" translatable="yes">Negation (¬&lt;sub&gt;e&lt;/sub&gt;)</property>
1579                                                 <property name="use_markup">True</property>
1580                                               </widget>
1581                                             </child>
1582                                           </widget>
1583                                           <packing>
1584                                             <property name="position">4</property>
1585                                           </packing>
1586                                         </child>
1587                                         <child>
1588                                           <widget class="GtkButton" id="butBot_elim">
1589                                             <property name="visible">True</property>
1590                                             <property name="can_focus">True</property>
1591                                             <property name="receives_default">True</property>
1592                                             <property name="response_id">0</property>
1593                                             <child>
1594                                               <widget class="GtkLabel" id="label33">
1595                                                 <property name="visible">True</property>
1596                                                 <property name="label" translatable="yes">Bottom (⊥&lt;sub&gt;e&lt;/sub&gt;)</property>
1597                                                 <property name="use_markup">True</property>
1598                                               </widget>
1599                                             </child>
1600                                           </widget>
1601                                           <packing>
1602                                             <property name="position">5</property>
1603                                           </packing>
1604                                         </child>
1605                                         <child>
1606                                           <widget class="GtkButton" id="butForall_elim">
1607                                             <property name="visible">True</property>
1608                                             <property name="can_focus">True</property>
1609                                             <property name="receives_default">True</property>
1610                                             <property name="response_id">0</property>
1611                                             <child>
1612                                               <widget class="GtkLabel" id="label34">
1613                                                 <property name="visible">True</property>
1614                                                 <property name="label" translatable="yes">Universal (∀&lt;sub&gt;e&lt;/sub&gt;)</property>
1615                                                 <property name="use_markup">True</property>
1616                                               </widget>
1617                                             </child>
1618                                           </widget>
1619                                           <packing>
1620                                             <property name="position">6</property>
1621                                           </packing>
1622                                         </child>
1623                                         <child>
1624                                           <widget class="GtkButton" id="butExists_elim">
1625                                             <property name="visible">True</property>
1626                                             <property name="can_focus">True</property>
1627                                             <property name="receives_default">True</property>
1628                                             <property name="response_id">0</property>
1629                                             <child>
1630                                               <widget class="GtkLabel" id="label35">
1631                                                 <property name="visible">True</property>
1632                                                 <property name="label" translatable="yes">Existential (∃&lt;sub&gt;e&lt;/sub&gt;)</property>
1633                                                 <property name="use_markup">True</property>
1634                                               </widget>
1635                                             </child>
1636                                           </widget>
1637                                           <packing>
1638                                             <property name="position">7</property>
1639                                           </packing>
1640                                         </child>
1641                                       </widget>
1642                                     </child>
1643                                     <child>
1644                                       <widget class="GtkLabel" id="label5">
1645                                         <property name="visible">True</property>
1646                                         <property name="label" translatable="yes">Elimination rules</property>
1647                                       </widget>
1648                                       <packing>
1649                                         <property name="type">label_item</property>
1650                                       </packing>
1651                                     </child>
1652                                   </widget>
1653                                   <packing>
1654                                     <property name="expand">False</property>
1655                                     <property name="position">1</property>
1656                                   </packing>
1657                                 </child>
1658                                 <child>
1659                                   <widget class="GtkExpander" id="expander3">
1660                                     <property name="visible">True</property>
1661                                     <property name="can_focus">True</property>
1662                                     <child>
1663                                       <widget class="GtkVBox" id="vbox4">
1664                                         <property name="visible">True</property>
1665                                         <child>
1666                                           <widget class="GtkButton" id="butRAA">
1667                                             <property name="visible">True</property>
1668                                             <property name="can_focus">True</property>
1669                                             <property name="receives_default">True</property>
1670                                             <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
1671                                             <property name="response_id">0</property>
1672                                           </widget>
1673                                         </child>
1674                                         <child>
1675                                           <widget class="GtkButton" id="butUseLemma">
1676                                             <property name="visible">True</property>
1677                                             <property name="can_focus">True</property>
1678                                             <property name="receives_default">True</property>
1679                                             <property name="label" translatable="yes">Use lemma (lem)</property>
1680                                             <property name="response_id">0</property>
1681                                           </widget>
1682                                           <packing>
1683                                             <property name="position">1</property>
1684                                           </packing>
1685                                         </child>
1686                                         <child>
1687                                           <widget class="GtkButton" id="butDischarge">
1688                                             <property name="visible">True</property>
1689                                             <property name="can_focus">True</property>
1690                                             <property name="receives_default">True</property>
1691                                             <property name="label" translatable="yes">Discharge (discharge)</property>
1692                                             <property name="response_id">0</property>
1693                                           </widget>
1694                                           <packing>
1695                                             <property name="position">2</property>
1696                                           </packing>
1697                                         </child>
1698                                       </widget>
1699                                     </child>
1700                                     <child>
1701                                       <widget class="GtkLabel" id="label6">
1702                                         <property name="visible">True</property>
1703                                         <property name="label" translatable="yes">Misc rules</property>
1704                                       </widget>
1705                                       <packing>
1706                                         <property name="type">label_item</property>
1707                                       </packing>
1708                                     </child>
1709                                   </widget>
1710                                   <packing>
1711                                     <property name="expand">False</property>
1712                                     <property name="position">2</property>
1713                                   </packing>
1714                                 </child>
1715                               </widget>
1716                             </child>
1717                           </widget>
1718                           <packing>
1719                             <property name="expand">False</property>
1720                           </packing>
1721                         </child>
1722                         <child>
1723                           <widget class="GtkVBox" id="vboxScript">
1724                             <property name="width_request">400</property>
1725                             <property name="visible">True</property>
1726                             <child>
1727                               <widget class="GtkHBox" id="hbox28">
1728                                 <property name="visible">True</property>
1729                                 <child>
1730                                   <widget class="GtkToolbar" id="buttonsToolbar">
1731                                     <property name="visible">True</property>
1732                                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1733                                     <child>
1734                                       <widget class="GtkToolItem" id="toolitem41">
1735                                         <property name="visible">True</property>
1736                                         <child>
1737                                           <widget class="GtkButton" id="scriptTopButton">
1738                                             <property name="visible">True</property>
1739                                             <property name="can_focus">True</property>
1740                                             <property name="tooltip" translatable="yes">Restart</property>
1741                                             <property name="relief">GTK_RELIEF_NONE</property>
1742                                             <property name="response_id">0</property>
1743                                             <child>
1744                                               <widget class="GtkImage" id="image920">
1745                                                 <property name="visible">True</property>
1746                                                 <property name="stock">gtk-goto-top</property>
1747                                               </widget>
1748                                             </child>
1749                                           </widget>
1750                                         </child>
1751                                       </widget>
1752                                       <packing>
1753                                         <property name="expand">False</property>
1754                                         <property name="homogeneous">False</property>
1755                                       </packing>
1756                                     </child>
1757                                     <child>
1758                                       <widget class="GtkToolItem" id="toolitem42">
1759                                         <property name="visible">True</property>
1760                                         <child>
1761                                           <widget class="GtkButton" id="scriptRetractButton">
1762                                             <property name="visible">True</property>
1763                                             <property name="can_focus">True</property>
1764                                             <property name="tooltip" translatable="yes">Retract 1 phrase</property>
1765                                             <property name="relief">GTK_RELIEF_NONE</property>
1766                                             <property name="response_id">0</property>
1767                                             <child>
1768                                               <widget class="GtkImage" id="image921">
1769                                                 <property name="visible">True</property>
1770                                                 <property name="stock">gtk-go-up</property>
1771                                               </widget>
1772                                             </child>
1773                                           </widget>
1774                                         </child>
1775                                       </widget>
1776                                       <packing>
1777                                         <property name="expand">False</property>
1778                                         <property name="homogeneous">False</property>
1779                                       </packing>
1780                                     </child>
1781                                     <child>
1782                                       <widget class="GtkToolItem" id="toolitem43">
1783                                         <property name="visible">True</property>
1784                                         <child>
1785                                           <widget class="GtkButton" id="scriptJumpButton">
1786                                             <property name="visible">True</property>
1787                                             <property name="can_focus">True</property>
1788                                             <property name="tooltip" translatable="yes">Execute until point</property>
1789                                             <property name="relief">GTK_RELIEF_NONE</property>
1790                                             <property name="response_id">0</property>
1791                                             <child>
1792                                               <widget class="GtkImage" id="image922">
1793                                                 <property name="visible">True</property>
1794                                                 <property name="stock">gtk-jump-to</property>
1795                                               </widget>
1796                                             </child>
1797                                           </widget>
1798                                         </child>
1799                                       </widget>
1800                                       <packing>
1801                                         <property name="expand">False</property>
1802                                         <property name="homogeneous">False</property>
1803                                       </packing>
1804                                     </child>
1805                                     <child>
1806                                       <widget class="GtkToolItem" id="toolitem44">
1807                                         <property name="visible">True</property>
1808                                         <child>
1809                                           <widget class="GtkButton" id="scriptAdvanceButton">
1810                                             <property name="visible">True</property>
1811                                             <property name="can_focus">True</property>
1812                                             <property name="tooltip" translatable="yes">Execute 1 phrase</property>
1813                                             <property name="relief">GTK_RELIEF_NONE</property>
1814                                             <property name="response_id">0</property>
1815                                             <child>
1816                                               <widget class="GtkImage" id="image923">
1817                                                 <property name="visible">True</property>
1818                                                 <property name="stock">gtk-go-down</property>
1819                                               </widget>
1820                                             </child>
1821                                           </widget>
1822                                         </child>
1823                                       </widget>
1824                                       <packing>
1825                                         <property name="expand">False</property>
1826                                         <property name="homogeneous">False</property>
1827                                       </packing>
1828                                     </child>
1829                                     <child>
1830                                       <widget class="GtkToolItem" id="toolitem45">
1831                                         <property name="visible">True</property>
1832                                         <child>
1833                                           <widget class="GtkButton" id="scriptBottomButton">
1834                                             <property name="visible">True</property>
1835                                             <property name="can_focus">True</property>
1836                                             <property name="tooltip" translatable="yes">Execute all</property>
1837                                             <property name="relief">GTK_RELIEF_NONE</property>
1838                                             <property name="response_id">0</property>
1839                                             <child>
1840                                               <widget class="GtkImage" id="image924">
1841                                                 <property name="visible">True</property>
1842                                                 <property name="stock">gtk-goto-bottom</property>
1843                                               </widget>
1844                                             </child>
1845                                           </widget>
1846                                         </child>
1847                                       </widget>
1848                                       <packing>
1849                                         <property name="expand">False</property>
1850                                         <property name="homogeneous">False</property>
1851                                       </packing>
1852                                     </child>
1853                                   </widget>
1854                                 </child>
1855                                 <child>
1856                                   <widget class="GtkToolbar" id="toolbar2">
1857                                     <property name="visible">True</property>
1858                                     <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
1859                                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1860                                     <child>
1861                                       <widget class="GtkToolItem" id="toolitem46">
1862                                         <property name="visible">True</property>
1863                                         <child>
1864                                           <widget class="GtkButton" id="scriptAbortButton">
1865                                             <property name="visible">True</property>
1866                                             <property name="can_focus">True</property>
1867                                             <property name="relief">GTK_RELIEF_NONE</property>
1868                                             <property name="response_id">0</property>
1869                                             <child>
1870                                               <widget class="GtkImage" id="image927">
1871                                                 <property name="visible">True</property>
1872                                                 <property name="stock">gtk-stop</property>
1873                                               </widget>
1874                                             </child>
1875                                           </widget>
1876                                         </child>
1877                                       </widget>
1878                                       <packing>
1879                                         <property name="expand">False</property>
1880                                         <property name="homogeneous">False</property>
1881                                       </packing>
1882                                     </child>
1883                                   </widget>
1884                                   <packing>
1885                                     <property name="expand">False</property>
1886                                     <property name="position">1</property>
1887                                   </packing>
1888                                 </child>
1889                               </widget>
1890                               <packing>
1891                                 <property name="expand">False</property>
1892                                 <property name="fill">False</property>
1893                               </packing>
1894                             </child>
1895                             <child>
1896                               <widget class="GtkNotebook" id="scriptNotebook">
1897                                 <property name="visible">True</property>
1898                                 <property name="can_focus">True</property>
1899                                 <property name="tab_pos">GTK_POS_BOTTOM</property>
1900                                 <child>
1901                                   <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
1902                                     <property name="visible">True</property>
1903                                     <property name="can_focus">True</property>
1904                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1905                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1906                                     <child>
1907                                       <placeholder/>
1908                                     </child>
1909                                   </widget>
1910                                 </child>
1911                                 <child>
1912                                   <widget class="GtkLabel" id="scriptLabel">
1913                                     <property name="visible">True</property>
1914                                     <property name="label" translatable="yes">script</property>
1915                                   </widget>
1916                                   <packing>
1917                                     <property name="type">tab</property>
1918                                     <property name="tab_fill">False</property>
1919                                   </packing>
1920                                 </child>
1921                                 <child>
1922                                   <widget class="GtkScrolledWindow" id="scrolledwindow8">
1923                                     <property name="visible">True</property>
1924                                     <property name="can_focus">True</property>
1925                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1926                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1927                                     <child>
1928                                       <widget class="GtkViewport" id="viewport1">
1929                                         <property name="visible">True</property>
1930                                         <child>
1931                                           <widget class="GtkLabel" id="label25">
1932                                             <property name="visible">True</property>
1933                                             <property name="label" translatable="yes">Not implemented.</property>
1934                                           </widget>
1935                                         </child>
1936                                       </widget>
1937                                     </child>
1938                                   </widget>
1939                                   <packing>
1940                                     <property name="position">1</property>
1941                                   </packing>
1942                                 </child>
1943                                 <child>
1944                                   <widget class="GtkLabel" id="label13">
1945                                     <property name="visible">True</property>
1946                                     <property name="label" translatable="yes">outline</property>
1947                                   </widget>
1948                                   <packing>
1949                                     <property name="type">tab</property>
1950                                     <property name="position">1</property>
1951                                     <property name="tab_fill">False</property>
1952                                   </packing>
1953                                 </child>
1954                               </widget>
1955                               <packing>
1956                                 <property name="position">1</property>
1957                               </packing>
1958                             </child>
1959                           </widget>
1960                           <packing>
1961                             <property name="position">1</property>
1962                           </packing>
1963                         </child>
1964                       </widget>
1965                       <packing>
1966                         <property name="resize">False</property>
1967                         <property name="shrink">True</property>
1968                       </packing>
1969                     </child>
1970                     <child>
1971                       <widget class="GtkVPaned" id="vpaned1">
1972                         <property name="width_request">250</property>
1973                         <property name="height_request">500</property>
1974                         <property name="visible">True</property>
1975                         <property name="can_focus">True</property>
1976                         <property name="position">380</property>
1977                         <child>
1978                           <widget class="GtkNotebook" id="sequentsNotebook">
1979                             <property name="visible">True</property>
1980                             <property name="can_focus">True</property>
1981                           </widget>
1982                           <packing>
1983                             <property name="resize">False</property>
1984                             <property name="shrink">True</property>
1985                           </packing>
1986                         </child>
1987                         <child>
1988                           <widget class="GtkHBox" id="hbox9">
1989                             <property name="visible">True</property>
1990                             <child>
1991                               <widget class="GtkScrolledWindow" id="logScrolledWin">
1992                                 <property name="visible">True</property>
1993                                 <property name="can_focus">True</property>
1994                                 <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
1995                                 <property name="shadow_type">GTK_SHADOW_IN</property>
1996                                 <child>
1997                                   <widget class="GtkTextView" id="logTextView">
1998                                     <property name="visible">True</property>
1999                                     <property name="can_focus">True</property>
2000                                     <property name="editable">False</property>
2001                                     <property name="wrap_mode">GTK_WRAP_CHAR</property>
2002                                     <property name="cursor_visible">False</property>
2003                                   </widget>
2004                                 </child>
2005                               </widget>
2006                             </child>
2007                           </widget>
2008                           <packing>
2009                             <property name="resize">True</property>
2010                             <property name="shrink">True</property>
2011                           </packing>
2012                         </child>
2013                       </widget>
2014                       <packing>
2015                         <property name="resize">True</property>
2016                         <property name="shrink">True</property>
2017                       </packing>
2018                     </child>
2019                   </widget>
2020                 </child>
2021               </widget>
2022               <packing>
2023                 <property name="position">1</property>
2024               </packing>
2025             </child>
2026             <child>
2027               <widget class="GtkHBox" id="hbox10">
2028                 <property name="visible">True</property>
2029                 <child>
2030                   <widget class="GtkStatusbar" id="StatusBar">
2031                     <property name="visible">True</property>
2032                     <property name="has_resize_grip">False</property>
2033                   </widget>
2034                 </child>
2035                 <child>
2036                   <widget class="GtkNotebook" id="HintNotebook">
2037                     <property name="visible">True</property>
2038                     <property name="show_tabs">False</property>
2039                     <child>
2040                       <widget class="GtkImage" id="HintLowImage">
2041                         <property name="visible">True</property>
2042                         <property name="stock">gtk-missing-image</property>
2043                       </widget>
2044                     </child>
2045                     <child>
2046                       <widget class="GtkLabel" id="label14">
2047                         <property name="visible">True</property>
2048                         <property name="label" translatable="yes">label14</property>
2049                       </widget>
2050                       <packing>
2051                         <property name="type">tab</property>
2052                         <property name="tab_fill">False</property>
2053                       </packing>
2054                     </child>
2055                     <child>
2056                       <widget class="GtkImage" id="HintMediumImage">
2057                         <property name="visible">True</property>
2058                         <property name="stock">gtk-missing-image</property>
2059                       </widget>
2060                       <packing>
2061                         <property name="position">1</property>
2062                       </packing>
2063                     </child>
2064                     <child>
2065                       <widget class="GtkLabel" id="label15">
2066                         <property name="visible">True</property>
2067                         <property name="label" translatable="yes">label15</property>
2068                       </widget>
2069                       <packing>
2070                         <property name="type">tab</property>
2071                         <property name="position">1</property>
2072                         <property name="tab_fill">False</property>
2073                       </packing>
2074                     </child>
2075                     <child>
2076                       <widget class="GtkImage" id="HintHighImage">
2077                         <property name="visible">True</property>
2078                         <property name="stock">gtk-missing-image</property>
2079                       </widget>
2080                       <packing>
2081                         <property name="position">2</property>
2082                       </packing>
2083                     </child>
2084                     <child>
2085                       <widget class="GtkLabel" id="label16">
2086                         <property name="visible">True</property>
2087                         <property name="label" translatable="yes">label16</property>
2088                       </widget>
2089                       <packing>
2090                         <property name="type">tab</property>
2091                         <property name="position">2</property>
2092                         <property name="tab_fill">False</property>
2093                       </packing>
2094                     </child>
2095                   </widget>
2096                   <packing>
2097                     <property name="expand">False</property>
2098                     <property name="position">1</property>
2099                   </packing>
2100                 </child>
2101               </widget>
2102               <packing>
2103                 <property name="expand">False</property>
2104                 <property name="fill">False</property>
2105                 <property name="position">2</property>
2106               </packing>
2107             </child>
2108           </widget>
2109         </child>
2110       </widget>
2111     </child>
2112   </widget>
2113   <widget class="GtkDialog" id="TextDialog">
2114     <property name="title" translatable="yes">DUMMY</property>
2115     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2116     <child internal-child="vbox">
2117       <widget class="GtkVBox" id="vbox5">
2118         <property name="visible">True</property>
2119         <child>
2120           <widget class="GtkLabel" id="TextDialogLabel">
2121             <property name="visible">True</property>
2122             <property name="label" translatable="yes">DUMMY</property>
2123           </widget>
2124           <packing>
2125             <property name="expand">False</property>
2126             <property name="fill">False</property>
2127             <property name="position">2</property>
2128           </packing>
2129         </child>
2130         <child>
2131           <widget class="GtkScrolledWindow" id="scrolledwindow2">
2132             <property name="visible">True</property>
2133             <property name="can_focus">True</property>
2134             <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2135             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2136             <property name="shadow_type">GTK_SHADOW_IN</property>
2137             <child>
2138               <widget class="GtkTextView" id="TextDialogTextView">
2139                 <property name="visible">True</property>
2140                 <property name="can_focus">True</property>
2141               </widget>
2142             </child>
2143           </widget>
2144           <packing>
2145             <property name="position">3</property>
2146           </packing>
2147         </child>
2148         <child internal-child="action_area">
2149           <widget class="GtkHButtonBox" id="hbuttonbox1">
2150             <property name="visible">True</property>
2151             <property name="layout_style">GTK_BUTTONBOX_END</property>
2152             <child>
2153               <widget class="GtkButton" id="TextDialogCancelButton">
2154                 <property name="visible">True</property>
2155                 <property name="can_focus">True</property>
2156                 <property name="can_default">True</property>
2157                 <property name="label">gtk-cancel</property>
2158                 <property name="use_stock">True</property>
2159                 <property name="response_id">-6</property>
2160               </widget>
2161             </child>
2162             <child>
2163               <widget class="GtkButton" id="TextDialogOkButton">
2164                 <property name="visible">True</property>
2165                 <property name="can_focus">True</property>
2166                 <property name="can_default">True</property>
2167                 <property name="label">gtk-ok</property>
2168                 <property name="use_stock">True</property>
2169                 <property name="response_id">-5</property>
2170               </widget>
2171               <packing>
2172                 <property name="position">1</property>
2173               </packing>
2174             </child>
2175           </widget>
2176           <packing>
2177             <property name="expand">False</property>
2178             <property name="pack_type">GTK_PACK_END</property>
2179           </packing>
2180         </child>
2181       </widget>
2182     </child>
2183   </widget>
2184   <widget class="GtkDialog" id="UriChoiceDialog">
2185     <property name="height_request">280</property>
2186     <property name="title" translatable="yes">Uri choice</property>
2187     <property name="modal">True</property>
2188     <property name="window_position">GTK_WIN_POS_CENTER</property>
2189     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2190     <child internal-child="vbox">
2191       <widget class="GtkVBox" id="dialog-vbox3">
2192         <property name="visible">True</property>
2193         <property name="spacing">4</property>
2194         <child>
2195           <widget class="GtkVBox" id="vbox2">
2196             <property name="visible">True</property>
2197             <property name="spacing">3</property>
2198             <child>
2199               <widget class="GtkLabel" id="UriChoiceLabel">
2200                 <property name="visible">True</property>
2201                 <property name="label" translatable="yes">some informative message here ...</property>
2202               </widget>
2203               <packing>
2204                 <property name="expand">False</property>
2205                 <property name="fill">False</property>
2206               </packing>
2207             </child>
2208             <child>
2209               <widget class="GtkScrolledWindow" id="scrolledwindow1">
2210                 <property name="width_request">400</property>
2211                 <property name="visible">True</property>
2212                 <property name="can_focus">True</property>
2213                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2214                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2215                 <child>
2216                   <widget class="GtkTreeView" id="UriChoiceTreeView">
2217                     <property name="visible">True</property>
2218                     <property name="can_focus">True</property>
2219                     <property name="headers_visible">False</property>
2220                   </widget>
2221                 </child>
2222               </widget>
2223               <packing>
2224                 <property name="position">1</property>
2225               </packing>
2226             </child>
2227             <child>
2228               <widget class="GtkHBox" id="uriEntryHBox">
2229                 <property name="visible">True</property>
2230                 <child>
2231                   <widget class="GtkLabel" id="label2">
2232                     <property name="visible">True</property>
2233                     <property name="label" translatable="yes">URI: </property>
2234                   </widget>
2235                   <packing>
2236                     <property name="expand">False</property>
2237                     <property name="fill">False</property>
2238                   </packing>
2239                 </child>
2240                 <child>
2241                   <widget class="GtkEntry" id="entry1">
2242                     <property name="visible">True</property>
2243                     <property name="can_focus">True</property>
2244                     <property name="invisible_char">*</property>
2245                   </widget>
2246                   <packing>
2247                     <property name="position">1</property>
2248                   </packing>
2249                 </child>
2250               </widget>
2251               <packing>
2252                 <property name="expand">False</property>
2253                 <property name="position">2</property>
2254               </packing>
2255             </child>
2256           </widget>
2257           <packing>
2258             <property name="position">2</property>
2259           </packing>
2260         </child>
2261         <child internal-child="action_area">
2262           <widget class="GtkHButtonBox" id="dialog-action_area3">
2263             <property name="visible">True</property>
2264             <property name="layout_style">GTK_BUTTONBOX_END</property>
2265             <child>
2266               <widget class="GtkButton" id="UriChoiceAbortButton">
2267                 <property name="visible">True</property>
2268                 <property name="can_focus">True</property>
2269                 <property name="can_default">True</property>
2270                 <property name="label">gtk-cancel</property>
2271                 <property name="use_stock">True</property>
2272                 <property name="response_id">-6</property>
2273               </widget>
2274             </child>
2275             <child>
2276               <widget class="GtkButton" id="UriChoiceSelectedButton">
2277                 <property name="visible">True</property>
2278                 <property name="can_focus">True</property>
2279                 <property name="can_default">True</property>
2280                 <property name="response_id">0</property>
2281                 <child>
2282                   <widget class="GtkAlignment" id="alignment2">
2283                     <property name="visible">True</property>
2284                     <property name="xscale">0</property>
2285                     <property name="yscale">0</property>
2286                     <child>
2287                       <widget class="GtkHBox" id="hbox3">
2288                         <property name="visible">True</property>
2289                         <property name="spacing">2</property>
2290                         <child>
2291                           <widget class="GtkImage" id="image19">
2292                             <property name="visible">True</property>
2293                             <property name="stock">gtk-index</property>
2294                           </widget>
2295                           <packing>
2296                             <property name="expand">False</property>
2297                             <property name="fill">False</property>
2298                           </packing>
2299                         </child>
2300                         <child>
2301                           <widget class="GtkLabel" id="label3">
2302                             <property name="visible">True</property>
2303                             <property name="label" translatable="yes">Try _Selected</property>
2304                             <property name="use_underline">True</property>
2305                           </widget>
2306                           <packing>
2307                             <property name="expand">False</property>
2308                             <property name="fill">False</property>
2309                             <property name="position">1</property>
2310                           </packing>
2311                         </child>
2312                       </widget>
2313                     </child>
2314                   </widget>
2315                 </child>
2316               </widget>
2317               <packing>
2318                 <property name="position">1</property>
2319               </packing>
2320             </child>
2321             <child>
2322               <widget class="GtkButton" id="UriChoiceConstantsButton">
2323                 <property name="visible">True</property>
2324                 <property name="sensitive">False</property>
2325                 <property name="can_focus">True</property>
2326                 <property name="can_default">True</property>
2327                 <property name="label" translatable="yes">Try Constants</property>
2328                 <property name="use_underline">True</property>
2329                 <property name="response_id">0</property>
2330               </widget>
2331               <packing>
2332                 <property name="position">2</property>
2333               </packing>
2334             </child>
2335             <child>
2336               <widget class="GtkButton" id="copyButton">
2337                 <property name="can_focus">True</property>
2338                 <property name="can_default">True</property>
2339                 <property name="label">gtk-copy</property>
2340                 <property name="use_stock">True</property>
2341                 <property name="response_id">0</property>
2342               </widget>
2343               <packing>
2344                 <property name="position">3</property>
2345               </packing>
2346             </child>
2347             <child>
2348               <widget class="GtkButton" id="uriChoiceAutoButton">
2349                 <property name="visible">True</property>
2350                 <property name="can_focus">True</property>
2351                 <property name="can_default">True</property>
2352                 <property name="response_id">0</property>
2353                 <child>
2354                   <widget class="GtkAlignment" id="alignment5">
2355                     <property name="visible">True</property>
2356                     <property name="xscale">0</property>
2357                     <property name="yscale">0</property>
2358                     <child>
2359                       <widget class="GtkHBox" id="hbox16">
2360                         <property name="visible">True</property>
2361                         <property name="spacing">2</property>
2362                         <child>
2363                           <widget class="GtkImage" id="image302">
2364                             <property name="visible">True</property>
2365                             <property name="stock">gtk-ok</property>
2366                           </widget>
2367                           <packing>
2368                             <property name="expand">False</property>
2369                             <property name="fill">False</property>
2370                           </packing>
2371                         </child>
2372                         <child>
2373                           <widget class="GtkLabel" id="okLabel">
2374                             <property name="visible">True</property>
2375                             <property name="label" translatable="yes">bla bla bla</property>
2376                             <property name="use_underline">True</property>
2377                           </widget>
2378                           <packing>
2379                             <property name="expand">False</property>
2380                             <property name="fill">False</property>
2381                             <property name="position">1</property>
2382                           </packing>
2383                         </child>
2384                       </widget>
2385                     </child>
2386                   </widget>
2387                 </child>
2388               </widget>
2389               <packing>
2390                 <property name="position">4</property>
2391               </packing>
2392             </child>
2393             <child>
2394               <widget class="GtkButton" id="uriChoiceForwardButton">
2395                 <property name="visible">True</property>
2396                 <property name="can_focus">True</property>
2397                 <property name="can_default">True</property>
2398                 <property name="label">gtk-go-forward</property>
2399                 <property name="use_stock">True</property>
2400                 <property name="response_id">0</property>
2401               </widget>
2402               <packing>
2403                 <property name="position">5</property>
2404               </packing>
2405             </child>
2406           </widget>
2407           <packing>
2408             <property name="expand">False</property>
2409             <property name="pack_type">GTK_PACK_END</property>
2410           </packing>
2411         </child>
2412       </widget>
2413     </child>
2414   </widget>
2415   <widget class="GtkWindow" id="FindReplWin">
2416     <property name="border_width">5</property>
2417     <property name="title" translatable="yes">Find &amp; Replace</property>
2418     <property name="resizable">False</property>
2419     <property name="window_position">GTK_WIN_POS_MOUSE</property>
2420     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2421     <child>
2422       <widget class="GtkTable" id="table1">
2423         <property name="visible">True</property>
2424         <property name="n_rows">3</property>
2425         <property name="n_columns">2</property>
2426         <property name="row_spacing">5</property>
2427         <child>
2428           <widget class="GtkLabel" id="label17">
2429             <property name="visible">True</property>
2430             <property name="xalign">0</property>
2431             <property name="label" translatable="yes">Find:</property>
2432           </widget>
2433           <packing>
2434             <property name="x_options"></property>
2435             <property name="y_options"></property>
2436           </packing>
2437         </child>
2438         <child>
2439           <widget class="GtkLabel" id="label18">
2440             <property name="visible">True</property>
2441             <property name="xalign">0</property>
2442             <property name="label" translatable="yes">Replace with: </property>
2443           </widget>
2444           <packing>
2445             <property name="top_attach">1</property>
2446             <property name="bottom_attach">2</property>
2447             <property name="x_options"></property>
2448             <property name="y_options"></property>
2449           </packing>
2450         </child>
2451         <child>
2452           <widget class="GtkEntry" id="findEntry">
2453             <property name="visible">True</property>
2454             <property name="can_focus">True</property>
2455             <property name="has_focus">True</property>
2456             <property name="can_default">True</property>
2457             <property name="has_default">True</property>
2458             <property name="invisible_char">*</property>
2459           </widget>
2460           <packing>
2461             <property name="left_attach">1</property>
2462             <property name="right_attach">2</property>
2463             <property name="y_options"></property>
2464           </packing>
2465         </child>
2466         <child>
2467           <widget class="GtkEntry" id="replaceEntry">
2468             <property name="visible">True</property>
2469             <property name="can_focus">True</property>
2470             <property name="invisible_char">*</property>
2471           </widget>
2472           <packing>
2473             <property name="left_attach">1</property>
2474             <property name="right_attach">2</property>
2475             <property name="top_attach">1</property>
2476             <property name="bottom_attach">2</property>
2477             <property name="y_options"></property>
2478           </packing>
2479         </child>
2480         <child>
2481           <widget class="GtkHBox" id="hbox19">
2482             <property name="visible">True</property>
2483             <property name="spacing">5</property>
2484             <child>
2485               <widget class="GtkVBox" id="vbox9">
2486                 <property name="visible">True</property>
2487                 <child>
2488                   <placeholder/>
2489                 </child>
2490                 <child>
2491                   <placeholder/>
2492                 </child>
2493               </widget>
2494             </child>
2495             <child>
2496               <widget class="GtkButton" id="findButton">
2497                 <property name="visible">True</property>
2498                 <property name="can_focus">True</property>
2499                 <property name="label">gtk-find</property>
2500                 <property name="use_stock">True</property>
2501                 <property name="response_id">0</property>
2502               </widget>
2503               <packing>
2504                 <property name="expand">False</property>
2505                 <property name="fill">False</property>
2506                 <property name="position">1</property>
2507               </packing>
2508             </child>
2509             <child>
2510               <widget class="GtkButton" id="findReplButton">
2511                 <property name="visible">True</property>
2512                 <property name="can_focus">True</property>
2513                 <property name="response_id">0</property>
2514                 <child>
2515                   <widget class="GtkAlignment" id="alignment13">
2516                     <property name="visible">True</property>
2517                     <property name="xscale">0</property>
2518                     <property name="yscale">0</property>
2519                     <child>
2520                       <widget class="GtkHBox" id="hbox20">
2521                         <property name="visible">True</property>
2522                         <property name="spacing">2</property>
2523                         <child>
2524                           <widget class="GtkImage" id="image357">
2525                             <property name="visible">True</property>
2526                             <property name="stock">gtk-find-and-replace</property>
2527                           </widget>
2528                           <packing>
2529                             <property name="expand">False</property>
2530                             <property name="fill">False</property>
2531                           </packing>
2532                         </child>
2533                         <child>
2534                           <widget class="GtkLabel" id="label19">
2535                             <property name="visible">True</property>
2536                             <property name="label">_Replace</property>
2537                             <property name="use_underline">True</property>
2538                           </widget>
2539                           <packing>
2540                             <property name="expand">False</property>
2541                             <property name="fill">False</property>
2542                             <property name="position">1</property>
2543                           </packing>
2544                         </child>
2545                       </widget>
2546                     </child>
2547                   </widget>
2548                 </child>
2549               </widget>
2550               <packing>
2551                 <property name="expand">False</property>
2552                 <property name="fill">False</property>
2553                 <property name="position">2</property>
2554               </packing>
2555             </child>
2556             <child>
2557               <widget class="GtkButton" id="cancelButton">
2558                 <property name="visible">True</property>
2559                 <property name="can_focus">True</property>
2560                 <property name="label">gtk-cancel</property>
2561                 <property name="use_stock">True</property>
2562                 <property name="response_id">0</property>
2563               </widget>
2564               <packing>
2565                 <property name="expand">False</property>
2566                 <property name="fill">False</property>
2567                 <property name="position">3</property>
2568               </packing>
2569             </child>
2570           </widget>
2571           <packing>
2572             <property name="right_attach">2</property>
2573             <property name="top_attach">2</property>
2574             <property name="bottom_attach">3</property>
2575             <property name="y_padding">5</property>
2576           </packing>
2577         </child>
2578       </widget>
2579     </child>
2580   </widget>
2581   <widget class="GtkDialog" id="DisambiguationErrors">
2582     <property name="width_request">450</property>
2583     <property name="height_request">400</property>
2584     <property name="title" translatable="yes">title</property>
2585     <property name="modal">True</property>
2586     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2587     <child internal-child="vbox">
2588       <widget class="GtkVBox" id="vbox14">
2589         <property name="visible">True</property>
2590         <child>
2591           <widget class="GtkVBox" id="vbox15">
2592             <property name="visible">True</property>
2593             <child>
2594               <widget class="GtkLabel" id="disambiguationErrorsLabel">
2595                 <property name="visible">True</property>
2596                 <property name="label" translatable="yes">some informative message here ...</property>
2597               </widget>
2598               <packing>
2599                 <property name="expand">False</property>
2600                 <property name="fill">False</property>
2601               </packing>
2602             </child>
2603             <child>
2604               <widget class="GtkScrolledWindow" id="scrolledwindow12">
2605                 <property name="visible">True</property>
2606                 <property name="can_focus">True</property>
2607                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2608                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2609                 <property name="shadow_type">GTK_SHADOW_IN</property>
2610                 <child>
2611                   <widget class="GtkTreeView" id="treeview">
2612                     <property name="visible">True</property>
2613                     <property name="can_focus">True</property>
2614                     <property name="headers_visible">False</property>
2615                   </widget>
2616                 </child>
2617               </widget>
2618               <packing>
2619                 <property name="position">1</property>
2620               </packing>
2621             </child>
2622           </widget>
2623           <packing>
2624             <property name="position">2</property>
2625           </packing>
2626         </child>
2627         <child internal-child="action_area">
2628           <widget class="GtkHButtonBox" id="hbuttonbox2">
2629             <property name="visible">True</property>
2630             <property name="layout_style">GTK_BUTTONBOX_END</property>
2631             <child>
2632               <widget class="GtkButton" id="button6">
2633                 <property name="visible">True</property>
2634                 <property name="can_focus">True</property>
2635                 <property name="can_default">True</property>
2636                 <property name="label">gtk-help</property>
2637                 <property name="use_stock">True</property>
2638                 <property name="response_id">-11</property>
2639               </widget>
2640             </child>
2641             <child>
2642               <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
2643                 <property name="visible">True</property>
2644                 <property name="can_focus">True</property>
2645                 <property name="can_default">True</property>
2646                 <property name="response_id">-6</property>
2647                 <child>
2648                   <widget class="GtkAlignment" id="alignment18">
2649                     <property name="visible">True</property>
2650                     <property name="xscale">0</property>
2651                     <property name="yscale">0</property>
2652                     <child>
2653                       <widget class="GtkHBox" id="hbox29">
2654                         <property name="visible">True</property>
2655                         <property name="spacing">2</property>
2656                         <child>
2657                           <widget class="GtkImage" id="image926">
2658                             <property name="visible">True</property>
2659                             <property name="stock">gtk-zoom-in</property>
2660                           </widget>
2661                           <packing>
2662                             <property name="expand">False</property>
2663                             <property name="fill">False</property>
2664                           </packing>
2665                         </child>
2666                         <child>
2667                           <widget class="GtkLabel" id="label28">
2668                             <property name="visible">True</property>
2669                             <property name="label">More</property>
2670                             <property name="use_underline">True</property>
2671                           </widget>
2672                           <packing>
2673                             <property name="expand">False</property>
2674                             <property name="fill">False</property>
2675                             <property name="position">1</property>
2676                           </packing>
2677                         </child>
2678                       </widget>
2679                     </child>
2680                   </widget>
2681                 </child>
2682               </widget>
2683               <packing>
2684                 <property name="position">1</property>
2685               </packing>
2686             </child>
2687             <child>
2688               <widget class="GtkButton" id="disambiguationErrorsCancelButton">
2689                 <property name="visible">True</property>
2690                 <property name="can_focus">True</property>
2691                 <property name="can_default">True</property>
2692                 <property name="has_default">True</property>
2693                 <property name="label">gtk-cancel</property>
2694                 <property name="use_stock">True</property>
2695                 <property name="response_id">-6</property>
2696               </widget>
2697               <packing>
2698                 <property name="position">2</property>
2699               </packing>
2700             </child>
2701             <child>
2702               <widget class="GtkButton" id="disambiguationErrorsOkButton">
2703                 <property name="visible">True</property>
2704                 <property name="can_focus">True</property>
2705                 <property name="can_default">True</property>
2706                 <property name="label">gtk-ok</property>
2707                 <property name="use_stock">True</property>
2708                 <property name="response_id">-5</property>
2709               </widget>
2710               <packing>
2711                 <property name="position">3</property>
2712               </packing>
2713             </child>
2714           </widget>
2715           <packing>
2716             <property name="expand">False</property>
2717             <property name="pack_type">GTK_PACK_END</property>
2718           </packing>
2719         </child>
2720       </widget>
2721     </child>
2722   </widget>
2723   <widget class="GtkWindow" id="AutoWin">
2724     <property name="width_request">600</property>
2725     <property name="height_request">400</property>
2726     <property name="visible">True</property>
2727     <property name="title" translatable="yes">Auto</property>
2728     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2729     <property name="gravity">GDK_GRAVITY_SOUTH_EAST</property>
2730     <child>
2731       <widget class="GtkVBox" id="vbox17">
2732         <property name="visible">True</property>
2733         <child>
2734           <widget class="GtkHBox" id="hbox30">
2735             <property name="visible">True</property>
2736             <property name="spacing">2</property>
2737             <child>
2738               <widget class="GtkScrolledWindow" id="scrolledwindowAREA">
2739                 <property name="visible">True</property>
2740                 <property name="can_focus">True</property>
2741                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2742                 <property name="shadow_type">GTK_SHADOW_IN</property>
2743                 <child>
2744                   <widget class="GtkViewport" id="viewportAREA">
2745                     <property name="visible">True</property>
2746                     <child>
2747                       <widget class="GtkTable" id="table">
2748                         <property name="visible">True</property>
2749                         <property name="n_rows">3</property>
2750                         <property name="n_columns">3</property>
2751                         <child>
2752                           <placeholder/>
2753                         </child>
2754                         <child>
2755                           <placeholder/>
2756                         </child>
2757                         <child>
2758                           <placeholder/>
2759                         </child>
2760                         <child>
2761                           <placeholder/>
2762                         </child>
2763                         <child>
2764                           <placeholder/>
2765                         </child>
2766                         <child>
2767                           <placeholder/>
2768                         </child>
2769                         <child>
2770                           <placeholder/>
2771                         </child>
2772                         <child>
2773                           <placeholder/>
2774                         </child>
2775                         <child>
2776                           <placeholder/>
2777                         </child>
2778                       </widget>
2779                     </child>
2780                   </widget>
2781                 </child>
2782               </widget>
2783             </child>
2784             <child>
2785               <widget class="GtkVBox" id="vbox18">
2786                 <property name="visible">True</property>
2787                 <child>
2788                   <widget class="GtkButton" id="buttonUP">
2789                     <property name="visible">True</property>
2790                     <property name="can_focus">True</property>
2791                     <property name="response_id">0</property>
2792                     <child>
2793                       <widget class="GtkAlignment" id="alignment19">
2794                         <property name="visible">True</property>
2795                         <property name="xscale">0</property>
2796                         <property name="yscale">0</property>
2797                         <child>
2798                           <widget class="GtkHBox" id="hbox31">
2799                             <property name="visible">True</property>
2800                             <property name="spacing">2</property>
2801                             <child>
2802                               <widget class="GtkImage" id="image1066">
2803                                 <property name="visible">True</property>
2804                                 <property name="stock">gtk-go-up</property>
2805                               </widget>
2806                               <packing>
2807                                 <property name="expand">False</property>
2808                                 <property name="fill">False</property>
2809                               </packing>
2810                             </child>
2811                             <child>
2812                               <widget class="GtkLabel" id="label30">
2813                                 <property name="visible">True</property>
2814                                 <property name="use_underline">True</property>
2815                               </widget>
2816                               <packing>
2817                                 <property name="expand">False</property>
2818                                 <property name="fill">False</property>
2819                                 <property name="position">1</property>
2820                               </packing>
2821                             </child>
2822                           </widget>
2823                         </child>
2824                       </widget>
2825                     </child>
2826                   </widget>
2827                 </child>
2828                 <child>
2829                   <widget class="GtkButton" id="buttonDOWN">
2830                     <property name="visible">True</property>
2831                     <property name="can_focus">True</property>
2832                     <property name="response_id">0</property>
2833                     <child>
2834                       <widget class="GtkImage" id="image1065">
2835                         <property name="visible">True</property>
2836                         <property name="stock">gtk-go-down</property>
2837                       </widget>
2838                     </child>
2839                   </widget>
2840                   <packing>
2841                     <property name="position">1</property>
2842                   </packing>
2843                 </child>
2844               </widget>
2845               <packing>
2846                 <property name="expand">False</property>
2847                 <property name="fill">False</property>
2848                 <property name="position">1</property>
2849               </packing>
2850             </child>
2851           </widget>
2852         </child>
2853         <child>
2854           <widget class="GtkHSeparator" id="hseparator3">
2855             <property name="visible">True</property>
2856           </widget>
2857           <packing>
2858             <property name="expand">False</property>
2859             <property name="padding">3</property>
2860             <property name="position">1</property>
2861           </packing>
2862         </child>
2863         <child>
2864           <widget class="GtkHBox" id="hbox32">
2865             <property name="visible">True</property>
2866             <child>
2867               <widget class="GtkLabel" id="labelLAST">
2868                 <property name="visible">True</property>
2869                 <property name="xalign">0</property>
2870                 <property name="label" translatable="yes">Last:</property>
2871               </widget>
2872             </child>
2873             <child>
2874               <widget class="GtkHButtonBox" id="hbuttonbox3">
2875                 <property name="visible">True</property>
2876                 <property name="border_width">4</property>
2877                 <property name="spacing">4</property>
2878                 <property name="layout_style">GTK_BUTTONBOX_END</property>
2879                 <child>
2880                   <widget class="GtkButton" id="buttonPAUSE">
2881                     <property name="visible">True</property>
2882                     <property name="can_focus">True</property>
2883                     <property name="can_default">True</property>
2884                     <property name="label">gtk-media-pause</property>
2885                     <property name="use_stock">True</property>
2886                     <property name="response_id">0</property>
2887                   </widget>
2888                 </child>
2889                 <child>
2890                   <widget class="GtkButton" id="buttonPLAY">
2891                     <property name="visible">True</property>
2892                     <property name="can_focus">True</property>
2893                     <property name="can_default">True</property>
2894                     <property name="label">gtk-media-play</property>
2895                     <property name="use_stock">True</property>
2896                     <property name="response_id">0</property>
2897                   </widget>
2898                   <packing>
2899                     <property name="position">1</property>
2900                   </packing>
2901                 </child>
2902                 <child>
2903                   <widget class="GtkButton" id="buttonNEXT">
2904                     <property name="visible">True</property>
2905                     <property name="can_focus">True</property>
2906                     <property name="can_default">True</property>
2907                     <property name="label">gtk-media-next</property>
2908                     <property name="use_stock">True</property>
2909                     <property name="response_id">0</property>
2910                   </widget>
2911                   <packing>
2912                     <property name="position">2</property>
2913                   </packing>
2914                 </child>
2915                 <child>
2916                   <widget class="GtkButton" id="buttonCLOSE">
2917                     <property name="visible">True</property>
2918                     <property name="can_focus">True</property>
2919                     <property name="can_default">True</property>
2920                     <property name="label">gtk-close</property>
2921                     <property name="use_stock">True</property>
2922                     <property name="response_id">0</property>
2923                   </widget>
2924                   <packing>
2925                     <property name="position">3</property>
2926                   </packing>
2927                 </child>
2928               </widget>
2929               <packing>
2930                 <property name="position">1</property>
2931               </packing>
2932             </child>
2933           </widget>
2934           <packing>
2935             <property name="expand">False</property>
2936             <property name="position">2</property>
2937           </packing>
2938         </child>
2939       </widget>
2940     </child>
2941   </widget>
2942 </glade-interface>