matita/matita/matita.ui

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