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