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