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="DisambiguationErrors">
 747     <property name="width_request">450</property>
 748     <property name="height_request">400</property>
 749     <property name="can_focus">False</property>
 750     <property name="title" translatable="yes">title</property>
 751     <property name="modal">True</property>
 752     <property name="type_hint">dialog</property>
 753     <child internal-child="vbox">
 754       <object class="GtkBox" id="vbox14">
 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="hbuttonbox2">
 760             <property name="visible">True</property>
 761             <property name="can_focus">False</property>
 762             <property name="layout_style">spread</property>
 763           </object>
 764           <packing>
 765             <property name="expand">False</property>
 766             <property name="fill">False</property>
 767             <property name="pack_type">end</property>
 768             <property name="position">0</property>
 769           </packing>
 770         </child>
 771         <child>
 772           <object class="GtkBox" id="vbox15">
 773             <property name="visible">True</property>
 774             <property name="can_focus">False</property>
 775             <property name="orientation">vertical</property>
 776             <child>
 777               <object class="GtkLabel" id="disambiguationErrorsLabel">
 778                 <property name="visible">True</property>
 779                 <property name="can_focus">False</property>
 780                 <property name="label" translatable="yes">some informative message here ...</property>
 781               </object>
 782               <packing>
 783                 <property name="expand">False</property>
 784                 <property name="fill">False</property>
 785                 <property name="position">0</property>
 786               </packing>
 787             </child>
 788             <child>
 789               <object class="GtkScrolledWindow" id="scrolledwindow12">
 790                 <property name="visible">True</property>
 791                 <property name="can_focus">True</property>
 792                 <property name="vexpand">True</property>
 793                 <property name="shadow_type">in</property>
 794                 <child>
 795                   <object class="GtkTreeView" id="treeview">
 796                     <property name="height_request">717</property>
 797                     <property name="visible">True</property>
 798                     <property name="can_focus">True</property>
 799                     <property name="headers_visible">False</property>
 800                     <child internal-child="selection">
 801                       <object class="GtkTreeSelection"/>
 802                     </child>
 803                   </object>
 804                 </child>
 805               </object>
 806               <packing>
 807                 <property name="expand">True</property>
 808                 <property name="fill">True</property>
 809                 <property name="position">1</property>
 810               </packing>
 811             </child>
 812           </object>
 813           <packing>
 814             <property name="expand">False</property>
 815             <property name="fill">True</property>
 816             <property name="position">2</property>
 817           </packing>
 818         </child>
 819       </object>
 820     </child>
 821   </object>
 822   <object class="GtkWindow" id="FindReplWin">
 823     <property name="can_focus">False</property>
 824     <property name="border_width">5</property>
 825     <property name="title" translatable="yes">Find &amp; Replace</property>
 826     <property name="resizable">False</property>
 827     <property name="window_position">mouse</property>
 828     <property name="type_hint">dialog</property>
 829     <child>
 830       <object class="GtkGrid" id="table1">
 831         <property name="visible">True</property>
 832         <property name="can_focus">False</property>
 833         <property name="row_spacing">9</property>
 834         <child>
 835           <object class="GtkLabel" id="label17">
 836             <property name="visible">True</property>
 837             <property name="can_focus">False</property>
 838             <property name="label" translatable="yes">Find:</property>
 839             <property name="xalign">0</property>
 840           </object>
 841           <packing>
 842             <property name="left_attach">0</property>
 843             <property name="top_attach">0</property>
 844           </packing>
 845         </child>
 846         <child>
 847           <object class="GtkLabel" id="label18">
 848             <property name="visible">True</property>
 849             <property name="can_focus">False</property>
 850             <property name="label" translatable="yes">Replace with: </property>
 851             <property name="xalign">0</property>
 852           </object>
 853           <packing>
 854             <property name="left_attach">0</property>
 855             <property name="top_attach">1</property>
 856           </packing>
 857         </child>
 858         <child>
 859           <object class="GtkEntry" id="findEntry">
 860             <property name="visible">True</property>
 861             <property name="can_focus">True</property>
 862             <property name="can_default">True</property>
 863             <property name="has_default">True</property>
 864           </object>
 865           <packing>
 866             <property name="left_attach">1</property>
 867             <property name="top_attach">0</property>
 868           </packing>
 869         </child>
 870         <child>
 871           <object class="GtkEntry" id="replaceEntry">
 872             <property name="visible">True</property>
 873             <property name="can_focus">True</property>
 874           </object>
 875           <packing>
 876             <property name="left_attach">1</property>
 877             <property name="top_attach">1</property>
 878           </packing>
 879         </child>
 880         <child>
 881           <object class="GtkBox" id="hbox19">
 882             <property name="visible">True</property>
 883             <property name="can_focus">False</property>
 884             <property name="spacing">5</property>
 885             <property name="homogeneous">True</property>
 886             <child>
 887               <object class="GtkButton" id="findButton">
 888                 <property name="label">gtk-find</property>
 889                 <property name="visible">True</property>
 890                 <property name="can_focus">True</property>
 891                 <property name="receives_default">False</property>
 892                 <property name="use_stock">True</property>
 893               </object>
 894               <packing>
 895                 <property name="expand">False</property>
 896                 <property name="fill">False</property>
 897                 <property name="position">1</property>
 898               </packing>
 899             </child>
 900             <child>
 901               <object class="GtkButton" id="findReplButton">
 902                 <property name="visible">True</property>
 903                 <property name="can_focus">True</property>
 904                 <property name="receives_default">False</property>
 905                 <child>
 906                   <object class="GtkAlignment" id="alignment13">
 907                     <property name="visible">True</property>
 908                     <property name="can_focus">False</property>
 909                     <property name="xscale">0</property>
 910                     <property name="yscale">0</property>
 911                     <child>
 912                       <object class="GtkBox" id="hbox20">
 913                         <property name="visible">True</property>
 914                         <property name="can_focus">False</property>
 915                         <property name="spacing">2</property>
 916                         <child>
 917                           <object class="GtkImage" id="image357">
 918                             <property name="visible">True</property>
 919                             <property name="can_focus">False</property>
 920                             <property name="stock">gtk-find-and-replace</property>
 921                           </object>
 922                           <packing>
 923                             <property name="expand">False</property>
 924                             <property name="fill">False</property>
 925                             <property name="position">0</property>
 926                           </packing>
 927                         </child>
 928                         <child>
 929                           <object class="GtkLabel" id="label19">
 930                             <property name="visible">True</property>
 931                             <property name="can_focus">False</property>
 932                             <property name="label">_Replace</property>
 933                             <property name="use_underline">True</property>
 934                           </object>
 935                           <packing>
 936                             <property name="expand">False</property>
 937                             <property name="fill">False</property>
 938                             <property name="position">1</property>
 939                           </packing>
 940                         </child>
 941                       </object>
 942                     </child>
 943                   </object>
 944                 </child>
 945               </object>
 946               <packing>
 947                 <property name="expand">False</property>
 948                 <property name="fill">False</property>
 949                 <property name="position">2</property>
 950               </packing>
 951             </child>
 952             <child>
 953               <object class="GtkButton" id="cancelButton">
 954                 <property name="label">gtk-cancel</property>
 955                 <property name="visible">True</property>
 956                 <property name="can_focus">True</property>
 957                 <property name="receives_default">False</property>
 958                 <property name="use_stock">True</property>
 959               </object>
 960               <packing>
 961                 <property name="expand">False</property>
 962                 <property name="fill">False</property>
 963                 <property name="position">3</property>
 964               </packing>
 965             </child>
 966           </object>
 967           <packing>
 968             <property name="left_attach">0</property>
 969             <property name="top_attach">2</property>
 970             <property name="width">2</property>
 971           </packing>
 972         </child>
 973       </object>
 974     </child>
 975   </object>
 976   <object class="GtkWindow" id="MainWin">
 977     <property name="can_focus">False</property>
 978     <property name="title" translatable="yes">Matita</property>
 979     <child>
 980       <object class="GtkEventBox" id="MainWinEventBox">
 981         <property name="visible">True</property>
 982         <property name="can_focus">False</property>
 983         <child>
 984           <object class="GtkBox" id="vbox8">
 985             <property name="visible">True</property>
 986             <property name="can_focus">False</property>
 987             <property name="orientation">vertical</property>
 988             <child>
 989               <object class="GtkMenuBar" id="menubar1">
 990                 <property name="visible">True</property>
 991                 <property name="can_focus">False</property>
 992                 <child>
 993                   <object class="GtkMenuItem" id="fileMenu">
 994                     <property name="visible">True</property>
 995                     <property name="can_focus">False</property>
 996                     <property name="label" translatable="yes">_File</property>
 997                     <property name="use_underline">True</property>
 998                     <child type="submenu">
 999                       <object class="GtkMenu" id="fileMenu_menu">
1000                         <property name="can_focus">False</property>
1001                         <child>
1002                           <object class="GtkMenuItem" id="newMenuItem">
1003                             <property name="visible">True</property>
1004                             <property name="can_focus">False</property>
1005                             <property name="label">_New</property>
1006                             <property name="use_underline">True</property>
1007                             <accelerator key="n" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1008                           </object>
1009                         </child>
1010                         <child>
1011                           <object class="GtkMenuItem" id="openMenuItem">
1012                             <property name="visible">True</property>
1013                             <property name="can_focus">False</property>
1014                             <property name="label">_Open...</property>
1015                             <property name="use_underline">True</property>
1016                             <accelerator key="o" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1017                           </object>
1018                         </child>
1019                         <child>
1020                           <object class="GtkMenuItem" id="saveMenuItem">
1021                             <property name="visible">True</property>
1022                             <property name="can_focus">False</property>
1023                             <property name="label">_Save</property>
1024                             <property name="use_underline">True</property>
1025                             <accelerator key="s" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1026                           </object>
1027                         </child>
1028                         <child>
1029                           <object class="GtkMenuItem" id="saveAsMenuItem">
1030                             <property name="visible">True</property>
1031                             <property name="can_focus">False</property>
1032                             <property name="label">_Save as...</property>
1033                             <property name="use_underline">True</property>
1034                             <accelerator key="s" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
1035                           </object>
1036                         </child>
1037                         <child>
1038                           <object class="GtkSeparatorMenuItem" id="separator2">
1039                             <property name="visible">True</property>
1040                             <property name="can_focus">False</property>
1041                           </object>
1042                         </child>
1043                         <child>
1044                           <object class="GtkMenuItem" id="closeMenuItem">
1045                             <property name="visible">True</property>
1046                             <property name="can_focus">False</property>
1047                             <property name="label">_Close</property>
1048                             <property name="use_underline">True</property>
1049                             <accelerator key="w" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1050                           </object>
1051                         </child>
1052                         <child>
1053                           <object class="GtkMenuItem" id="quitMenuItem">
1054                             <property name="visible">True</property>
1055                             <property name="can_focus">False</property>
1056                             <property name="label">_Quit</property>
1057                             <property name="use_underline">True</property>
1058                             <accelerator key="q" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1059                           </object>
1060                         </child>
1061                       </object>
1062                     </child>
1063                   </object>
1064                 </child>
1065                 <child>
1066                   <object class="GtkMenuItem" id="editMenu">
1067                     <property name="visible">True</property>
1068                     <property name="can_focus">False</property>
1069                     <property name="label" translatable="yes">_Edit</property>
1070                     <property name="use_underline">True</property>
1071                     <child type="submenu">
1072                       <object class="GtkMenu" id="editMenu_menu">
1073                         <property name="can_focus">False</property>
1074                         <child>
1075                           <object class="GtkMenuItem" id="undoMenuItem">
1076                             <property name="visible">True</property>
1077                             <property name="sensitive">False</property>
1078                             <property name="can_focus">False</property>
1079                             <property name="label">_Undo</property>
1080                             <property name="use_underline">True</property>
1081                             <accelerator key="z" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1082                           </object>
1083                         </child>
1084                         <child>
1085                           <object class="GtkMenuItem" id="redoMenuItem">
1086                             <property name="visible">True</property>
1087                             <property name="sensitive">False</property>
1088                             <property name="can_focus">False</property>
1089                             <property name="label">_Redo</property>
1090                             <property name="use_underline">True</property>
1091                             <accelerator key="z" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
1092                           </object>
1093                         </child>
1094                         <child>
1095                           <object class="GtkSeparatorMenuItem" id="separator3">
1096                             <property name="visible">True</property>
1097                             <property name="can_focus">False</property>
1098                           </object>
1099                         </child>
1100                         <child>
1101                           <object class="GtkMenuItem" id="cutMenuItem">
1102                             <property name="visible">True</property>
1103                             <property name="can_focus">False</property>
1104                             <property name="label">Cut</property>
1105                             <property name="use_underline">True</property>
1106                             <accelerator key="x" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1107                           </object>
1108                         </child>
1109                         <child>
1110                           <object class="GtkMenuItem" id="copyMenuItem">
1111                             <property name="visible">True</property>
1112                             <property name="can_focus">False</property>
1113                             <property name="label">Copy</property>
1114                             <property name="use_underline">True</property>
1115                             <accelerator key="c" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1116                           </object>
1117                         </child>
1118                         <child>
1119                           <object class="GtkMenuItem" id="pasteMenuItem">
1120                             <property name="visible">True</property>
1121                             <property name="can_focus">False</property>
1122                             <property name="label">Paste</property>
1123                             <property name="use_underline">True</property>
1124                             <accelerator key="v" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1125                           </object>
1126                         </child>
1127                         <child>
1128                           <object class="GtkMenuItem" id="pastePatternMenuItem">
1129                             <property name="visible">True</property>
1130                             <property name="can_focus">False</property>
1131                             <property name="label" translatable="yes">Paste as pattern</property>
1132                             <property name="use_underline">True</property>
1133                           </object>
1134                         </child>
1135                         <child>
1136                           <object class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
1137                             <property name="visible">True</property>
1138                             <property name="can_focus">False</property>
1139                             <property name="label" translatable="yes">Paste Unicode as TeX</property>
1140                             <property name="use_underline">True</property>
1141                           </object>
1142                         </child>
1143                         <child>
1144                           <object class="GtkCheckMenuItem" id="menuitemAutoAltL">
1145                             <property name="visible">True</property>
1146                             <property name="can_focus">False</property>
1147                             <property name="label" translatable="yes">Auto-expand TeX Macros</property>
1148                             <property name="use_underline">True</property>
1149                             <property name="active">True</property>
1150                           </object>
1151                         </child>
1152                         <child>
1153                           <object class="GtkMenuItem" id="deleteMenuItem">
1154                             <property name="visible">True</property>
1155                             <property name="can_focus">False</property>
1156                             <property name="label">Delete</property>
1157                             <property name="use_underline">True</property>
1158                           </object>
1159                         </child>
1160                         <child>
1161                           <object class="GtkSeparatorMenuItem" id="separator4">
1162                             <property name="visible">True</property>
1163                             <property name="can_focus">False</property>
1164                           </object>
1165                         </child>
1166                         <child>
1167                           <object class="GtkMenuItem" id="selectAllMenuItem">
1168                             <property name="visible">True</property>
1169                             <property name="can_focus">False</property>
1170                             <property name="label" translatable="yes">Select _All</property>
1171                             <property name="use_underline">True</property>
1172                           </object>
1173                         </child>
1174                         <child>
1175                           <object class="GtkSeparatorMenuItem" id="separator7">
1176                             <property name="visible">True</property>
1177                             <property name="can_focus">False</property>
1178                           </object>
1179                         </child>
1180                         <child>
1181                           <object class="GtkMenuItem" id="findReplMenuItem">
1182                             <property name="visible">True</property>
1183                             <property name="can_focus">False</property>
1184                             <property name="label">Find and replace...</property>
1185                             <property name="use_underline">True</property>
1186                             <accelerator key="f" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1187                           </object>
1188                         </child>
1189                         <child>
1190                           <object class="GtkSeparatorMenuItem" id="separator8">
1191                             <property name="visible">True</property>
1192                             <property name="can_focus">False</property>
1193                           </object>
1194                         </child>
1195                         <child>
1196                           <object class="GtkMenuItem" id="LigatureButton">
1197                             <property name="visible">True</property>
1198                             <property name="can_focus">False</property>
1199                             <property name="label" translatable="yes">Next ligature</property>
1200                             <property name="use_underline">True</property>
1201                             <accelerator key="l" signal="activate" modifiers="GDK_MOD1_MASK"/>
1202                           </object>
1203                         </child>
1204                         <child>
1205                           <object class="GtkMenuItem" id="externalEditorMenuItem">
1206                             <property name="visible">True</property>
1207                             <property name="can_focus">False</property>
1208                             <property name="label" translatable="yes">Edit with e_xternal editor</property>
1209                             <property name="use_underline">True</property>
1210                           </object>
1211                         </child>
1212                       </object>
1213                     </child>
1214                   </object>
1215                 </child>
1216                 <child>
1217                   <object class="GtkMenuItem" id="scriptMenu">
1218                     <property name="visible">True</property>
1219                     <property name="can_focus">False</property>
1220                     <property name="label" translatable="yes">_Script</property>
1221                     <property name="use_underline">True</property>
1222                     <child type="submenu">
1223                       <object class="GtkMenu" id="scriptMenu_menu">
1224                         <property name="can_focus">False</property>
1225                         <child>
1226                           <object class="GtkMenuItem" id="scriptAdvanceMenuItem">
1227                             <property name="visible">True</property>
1228                             <property name="can_focus">False</property>
1229                             <property name="label">Execute 1 phrase</property>
1230                             <property name="use_underline">True</property>
1231                             <accelerator key="Page_Down" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
1232                           </object>
1233                         </child>
1234                         <child>
1235                           <object class="GtkMenuItem" id="scriptRetractMenuItem">
1236                             <property name="visible">True</property>
1237                             <property name="can_focus">False</property>
1238                             <property name="label">Retract 1 phrase</property>
1239                             <property name="use_underline">True</property>
1240                             <accelerator key="Page_Up" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
1241                           </object>
1242                         </child>
1243                         <child>
1244                           <object class="GtkSeparatorMenuItem" id="separator9">
1245                             <property name="visible">True</property>
1246                             <property name="can_focus">False</property>
1247                           </object>
1248                         </child>
1249                         <child>
1250                           <object class="GtkMenuItem" id="scriptBottomMenuItem">
1251                             <property name="visible">True</property>
1252                             <property name="can_focus">False</property>
1253                             <property name="label">Execute all</property>
1254                             <property name="use_underline">True</property>
1255                             <accelerator key="End" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
1256                           </object>
1257                         </child>
1258                         <child>
1259                           <object class="GtkMenuItem" id="scriptTopMenuItem">
1260                             <property name="visible">True</property>
1261                             <property name="can_focus">False</property>
1262                             <property name="label">Retract all</property>
1263                             <property name="use_underline">True</property>
1264                             <accelerator key="Home" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
1265                           </object>
1266                         </child>
1267                         <child>
1268                           <object class="GtkSeparatorMenuItem" id="separator10">
1269                             <property name="visible">True</property>
1270                             <property name="can_focus">False</property>
1271                           </object>
1272                         </child>
1273                         <child>
1274                           <object class="GtkMenuItem" id="scriptJumpMenuItem">
1275                             <property name="visible">True</property>
1276                             <property name="can_focus">False</property>
1277                             <property name="label">Execute until cursor</property>
1278                             <property name="use_underline">True</property>
1279                             <accelerator key="period" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
1280                           </object>
1281                         </child>
1282                       </object>
1283                     </child>
1284                   </object>
1285                 </child>
1286                 <child>
1287                   <object class="GtkMenuItem" id="viewMenu">
1288                     <property name="visible">True</property>
1289                     <property name="can_focus">False</property>
1290                     <property name="label" translatable="yes">_View</property>
1291                     <property name="use_underline">True</property>
1292                     <child type="submenu">
1293                       <object class="GtkMenu" id="viewMenu_menu">
1294                         <property name="can_focus">False</property>
1295                         <child>
1296                           <object class="GtkMenuItem" id="newCicBrowserMenuItem">
1297                             <property name="visible">True</property>
1298                             <property name="can_focus">False</property>
1299                             <property name="label" translatable="yes">New CIC _browser</property>
1300                             <property name="use_underline">True</property>
1301                             <accelerator key="F3" signal="activate"/>
1302                           </object>
1303                         </child>
1304                         <child>
1305                           <object class="GtkSeparatorMenuItem" id="separator5">
1306                             <property name="visible">True</property>
1307                             <property name="can_focus">False</property>
1308                           </object>
1309                         </child>
1310                         <child>
1311                           <object class="GtkCheckMenuItem" id="fullscreenMenuItem">
1312                             <property name="visible">True</property>
1313                             <property name="can_focus">False</property>
1314                             <property name="label" translatable="yes">_Fullscreen</property>
1315                             <property name="use_underline">True</property>
1316                             <accelerator key="F11" signal="activate"/>
1317                           </object>
1318                         </child>
1319                         <child>
1320                           <object class="GtkCheckMenuItem" id="menuitemPalette">
1321                             <property name="visible">True</property>
1322                             <property name="can_focus">False</property>
1323                             <property name="label" translatable="yes">Natural deduction palette</property>
1324                             <property name="use_underline">True</property>
1325                             <accelerator key="F2" signal="activate"/>
1326                           </object>
1327                         </child>
1328                         <child>
1329                           <object class="GtkSeparatorMenuItem" id="separator1">
1330                             <property name="visible">True</property>
1331                             <property name="can_focus">False</property>
1332                           </object>
1333                         </child>
1334                         <child>
1335                           <object class="GtkMenuItem" id="increaseFontSizeMenuItem">
1336                             <property name="visible">True</property>
1337                             <property name="can_focus">False</property>
1338                             <property name="label">Zoom in</property>
1339                             <property name="use_underline">True</property>
1340                             <accelerator key="plus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1341                           </object>
1342                         </child>
1343                         <child>
1344                           <object class="GtkMenuItem" id="decreaseFontSizeMenuItem">
1345                             <property name="visible">True</property>
1346                             <property name="can_focus">False</property>
1347                             <property name="label">Zoom out</property>
1348                             <property name="use_underline">True</property>
1349                             <accelerator key="minus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1350                           </object>
1351                         </child>
1352                         <child>
1353                           <object class="GtkMenuItem" id="normalFontSizeMenuItem">
1354                             <property name="visible">True</property>
1355                             <property name="can_focus">False</property>
1356                             <property name="label">Normal size</property>
1357                             <property name="use_underline">True</property>
1358                             <accelerator key="equal" signal="activate" modifiers="GDK_CONTROL_MASK"/>
1359                           </object>
1360                         </child>
1361                         <child>
1362                           <object class="GtkSeparatorMenuItem" id="separator12">
1363                             <property name="visible">True</property>
1364                             <property name="can_focus">False</property>
1365                           </object>
1366                         </child>
1367                         <child>
1368                           <object class="GtkCheckMenuItem" id="ppNotationMenuItem">
1369                             <property name="visible">True</property>
1370                             <property name="can_focus">False</property>
1371                             <property name="label" translatable="yes">Pretty print notation</property>
1372                             <property name="use_underline">True</property>
1373                             <property name="active">True</property>
1374                           </object>
1375                         </child>
1376                         <child>
1377                           <object class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
1378                             <property name="visible">True</property>
1379                             <property name="can_focus">False</property>
1380                             <property name="label" translatable="yes">Hide coercions</property>
1381                             <property name="use_underline">True</property>
1382                             <property name="active">True</property>
1383                           </object>
1384                         </child>
1385                         <child>
1386                           <object class="GtkSeparatorMenuItem" id="separator13">
1387                             <property name="visible">True</property>
1388                             <property name="can_focus">False</property>
1389                           </object>
1390                         </child>
1391                         <child>
1392                           <object class="GtkMenuItem" id="showCoercionsGraphMenuItem">
1393                             <property name="visible">True</property>
1394                             <property name="can_focus">False</property>
1395                             <property name="label" translatable="yes">Coercions Graph</property>
1396                             <property name="use_underline">True</property>
1397                           </object>
1398                         </child>
1399                         <child>
1400                           <object class="GtkMenuItem" id="showHintsDbMenuItem">
1401                             <property name="visible">True</property>
1402                             <property name="can_focus">False</property>
1403                             <property name="label" translatable="yes">Hints database</property>
1404                             <property name="use_underline">True</property>
1405                           </object>
1406                         </child>
1407                         <child>
1408                           <object class="GtkMenuItem" id="showTermGrammarMenuItem">
1409                             <property name="visible">True</property>
1410                             <property name="can_focus">False</property>
1411                             <property name="label" translatable="yes">Terms grammar</property>
1412                             <property name="use_underline">True</property>
1413                           </object>
1414                         </child>
1415                         <child>
1416                           <object class="GtkMenuItem" id="showUnicodeTable">
1417                             <property name="visible">True</property>
1418                             <property name="can_focus">False</property>
1419                             <property name="label" translatable="yes">TeX/UTF-8 table</property>
1420                             <property name="use_underline">True</property>
1421                           </object>
1422                         </child>
1423                       </object>
1424                     </child>
1425                   </object>
1426                 </child>
1427                 <child>
1428                   <object class="GtkMenuItem" id="debugMenu">
1429                     <property name="visible">True</property>
1430                     <property name="can_focus">False</property>
1431                     <property name="label" translatable="yes">_Debug</property>
1432                     <property name="use_underline">True</property>
1433                     <child type="submenu">
1434                       <object class="GtkMenu" id="debugMenu_menu">
1435                         <property name="can_focus">False</property>
1436                         <child>
1437                           <object class="GtkSeparatorMenuItem" id="separator6">
1438                             <property name="visible">True</property>
1439                             <property name="can_focus">False</property>
1440                           </object>
1441                         </child>
1442                       </object>
1443                     </child>
1444                   </object>
1445                 </child>
1446                 <child>
1447                   <object class="GtkMenuItem" id="helpMenu">
1448                     <property name="visible">True</property>
1449                     <property name="can_focus">False</property>
1450                     <property name="label" translatable="yes">_Help</property>
1451                     <property name="use_underline">True</property>
1452                     <child type="submenu">
1453                       <object class="GtkMenu" id="helpMenu_menu">
1454                         <property name="can_focus">False</property>
1455                         <child>
1456                           <object class="GtkMenuItem" id="contentsMenuItem">
1457                             <property name="visible">True</property>
1458                             <property name="can_focus">False</property>
1459                             <property name="label">Contents</property>
1460                             <property name="use_underline">True</property>
1461                             <accelerator key="F1" signal="activate"/>
1462                           </object>
1463                         </child>
1464                         <child>
1465                           <object class="GtkMenuItem" id="aboutMenuItem">
1466                             <property name="visible">True</property>
1467                             <property name="can_focus">False</property>
1468                             <property name="label">About</property>
1469                             <property name="use_underline">True</property>
1470                           </object>
1471                         </child>
1472                       </object>
1473                     </child>
1474                   </object>
1475                 </child>
1476               </object>
1477               <packing>
1478                 <property name="expand">False</property>
1479                 <property name="fill">False</property>
1480                 <property name="position">0</property>
1481               </packing>
1482             </child>
1483             <child>
1484               <object class="GtkBox" id="hbox99">
1485                 <property name="visible">True</property>
1486                 <property name="can_focus">False</property>
1487                 <child>
1488                   <object class="GtkPaned" id="hpaneScriptSequent">
1489                     <property name="visible">True</property>
1490                     <property name="can_focus">True</property>
1491                     <child>
1492                       <object class="GtkBox" id="hbox18">
1493                         <property name="visible">True</property>
1494                         <property name="can_focus">False</property>
1495                         <property name="spacing">2</property>
1496                         <child>
1497                           <object class="GtkBox" id="TacticsButtonsHandlebox">
1498                             <property name="visible">True</property>
1499                             <property name="can_focus">False</property>
1500                             <child>
1501                               <object class="GtkBox" id="vboxTacticsPalette">
1502                                 <property name="visible">True</property>
1503                                 <property name="can_focus">False</property>
1504                                 <property name="orientation">vertical</property>
1505                                 <child>
1506                                   <object class="GtkExpander" id="expander1">
1507                                     <property name="visible">True</property>
1508                                     <property name="can_focus">True</property>
1509                                     <child>
1510                                       <object class="GtkBox" id="vbox1">
1511                                         <property name="visible">True</property>
1512                                         <property name="can_focus">False</property>
1513                                         <property name="orientation">vertical</property>
1514                                         <child>
1515                                           <object class="GtkButton" id="butImpl_intro">
1516                                             <property name="visible">True</property>
1517                                             <property name="can_focus">True</property>
1518                                             <property name="receives_default">True</property>
1519                                             <child>
1520                                               <object class="GtkLabel" id="label8">
1521                                                 <property name="visible">True</property>
1522                                                 <property name="can_focus">False</property>
1523                                                 <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;i&lt;/sub&gt;)</property>
1524                                                 <property name="use_markup">True</property>
1525                                               </object>
1526                                             </child>
1527                                           </object>
1528                                           <packing>
1529                                             <property name="expand">True</property>
1530                                             <property name="fill">True</property>
1531                                             <property name="position">0</property>
1532                                           </packing>
1533                                         </child>
1534                                         <child>
1535                                           <object class="GtkButton" id="butAnd_intro">
1536                                             <property name="visible">True</property>
1537                                             <property name="can_focus">True</property>
1538                                             <property name="receives_default">True</property>
1539                                             <child>
1540                                               <object class="GtkLabel" id="label7">
1541                                                 <property name="visible">True</property>
1542                                                 <property name="can_focus">False</property>
1543                                                 <property name="label" translatable="yes">Conjunction (∧&lt;sub&gt;i&lt;/sub&gt;)</property>
1544                                                 <property name="use_markup">True</property>
1545                                               </object>
1546                                             </child>
1547                                           </object>
1548                                           <packing>
1549                                             <property name="expand">True</property>
1550                                             <property name="fill">True</property>
1551                                             <property name="position">1</property>
1552                                           </packing>
1553                                         </child>
1554                                         <child>
1555                                           <object class="GtkButton" id="butOr_intro_left">
1556                                             <property name="visible">True</property>
1557                                             <property name="can_focus">True</property>
1558                                             <property name="receives_default">True</property>
1559                                             <child>
1560                                               <object class="GtkLabel" id="label9">
1561                                                 <property name="visible">True</property>
1562                                                 <property name="can_focus">False</property>
1563                                                 <property name="label" translatable="yes">Disjunction left (∨&lt;sub&gt;i-l&lt;/sub&gt;)</property>
1564                                                 <property name="use_markup">True</property>
1565                                               </object>
1566                                             </child>
1567                                           </object>
1568                                           <packing>
1569                                             <property name="expand">True</property>
1570                                             <property name="fill">True</property>
1571                                             <property name="position">2</property>
1572                                           </packing>
1573                                         </child>
1574                                         <child>
1575                                           <object class="GtkButton" id="butOr_intro_right">
1576                                             <property name="visible">True</property>
1577                                             <property name="can_focus">True</property>
1578                                             <property name="receives_default">True</property>
1579                                             <child>
1580                                               <object class="GtkLabel" id="label10">
1581                                                 <property name="visible">True</property>
1582                                                 <property name="can_focus">False</property>
1583                                                 <property name="label" translatable="yes">Disjunction right (∨&lt;sub&gt;i-r&lt;/sub&gt;)</property>
1584                                                 <property name="use_markup">True</property>
1585                                               </object>
1586                                             </child>
1587                                           </object>
1588                                           <packing>
1589                                             <property name="expand">True</property>
1590                                             <property name="fill">True</property>
1591                                             <property name="position">3</property>
1592                                           </packing>
1593                                         </child>
1594                                         <child>
1595                                           <object class="GtkButton" id="butNot_intro">
1596                                             <property name="visible">True</property>
1597                                             <property name="can_focus">True</property>
1598                                             <property name="receives_default">True</property>
1599                                             <child>
1600                                               <object class="GtkLabel" id="label11">
1601                                                 <property name="visible">True</property>
1602                                                 <property name="can_focus">False</property>
1603                                                 <property name="label" translatable="yes">Negation (¬&lt;sub&gt;i&lt;/sub&gt;)</property>
1604                                                 <property name="use_markup">True</property>
1605                                               </object>
1606                                             </child>
1607                                           </object>
1608                                           <packing>
1609                                             <property name="expand">True</property>
1610                                             <property name="fill">True</property>
1611                                             <property name="position">4</property>
1612                                           </packing>
1613                                         </child>
1614                                         <child>
1615                                           <object class="GtkButton" id="butTop_intro">
1616                                             <property name="visible">True</property>
1617                                             <property name="can_focus">True</property>
1618                                             <property name="receives_default">True</property>
1619                                             <child>
1620                                               <object class="GtkLabel" id="label12">
1621                                                 <property name="visible">True</property>
1622                                                 <property name="can_focus">False</property>
1623                                                 <property name="label" translatable="yes">Top (⊤&lt;sub&gt;i&lt;/sub&gt;)</property>
1624                                                 <property name="use_markup">True</property>
1625                                               </object>
1626                                             </child>
1627                                           </object>
1628                                           <packing>
1629                                             <property name="expand">True</property>
1630                                             <property name="fill">True</property>
1631                                             <property name="position">5</property>
1632                                           </packing>
1633                                         </child>
1634                                         <child>
1635                                           <object class="GtkButton" id="butForall_intro">
1636                                             <property name="visible">True</property>
1637                                             <property name="can_focus">True</property>
1638                                             <property name="receives_default">True</property>
1639                                             <child>
1640                                               <object class="GtkLabel" id="label20">
1641                                                 <property name="visible">True</property>
1642                                                 <property name="can_focus">False</property>
1643                                                 <property name="label" translatable="yes">Universal (∀&lt;sub&gt;i&lt;/sub&gt;)</property>
1644                                                 <property name="use_markup">True</property>
1645                                               </object>
1646                                             </child>
1647                                           </object>
1648                                           <packing>
1649                                             <property name="expand">True</property>
1650                                             <property name="fill">True</property>
1651                                             <property name="position">6</property>
1652                                           </packing>
1653                                         </child>
1654                                         <child>
1655                                           <object class="GtkButton" id="butExists_intro">
1656                                             <property name="visible">True</property>
1657                                             <property name="can_focus">True</property>
1658                                             <property name="receives_default">True</property>
1659                                             <child>
1660                                               <object class="GtkLabel" id="label21">
1661                                                 <property name="visible">True</property>
1662                                                 <property name="can_focus">False</property>
1663                                                 <property name="label" translatable="yes">Existential (∃&lt;sub&gt;i&lt;/sub&gt;)</property>
1664                                                 <property name="use_markup">True</property>
1665                                               </object>
1666                                             </child>
1667                                           </object>
1668                                           <packing>
1669                                             <property name="expand">True</property>
1670                                             <property name="fill">True</property>
1671                                             <property name="position">7</property>
1672                                           </packing>
1673                                         </child>
1674                                       </object>
1675                                     </child>
1676                                     <child type="label">
1677                                       <object class="GtkLabel" id="label4">
1678                                         <property name="visible">True</property>
1679                                         <property name="can_focus">False</property>
1680                                         <property name="label" translatable="yes">Introduction rules</property>
1681                                       </object>
1682                                     </child>
1683                                   </object>
1684                                   <packing>
1685                                     <property name="expand">False</property>
1686                                     <property name="fill">True</property>
1687                                     <property name="position">0</property>
1688                                   </packing>
1689                                 </child>
1690                                 <child>
1691                                   <object class="GtkExpander" id="expander2">
1692                                     <property name="visible">True</property>
1693                                     <property name="can_focus">True</property>
1694                                     <child>
1695                                       <object class="GtkBox" id="vbox3">
1696                                         <property name="visible">True</property>
1697                                         <property name="can_focus">False</property>
1698                                         <property name="orientation">vertical</property>
1699                                         <child>
1700                                           <object class="GtkButton" id="butImpl_elim">
1701                                             <property name="visible">True</property>
1702                                             <property name="can_focus">True</property>
1703                                             <property name="receives_default">True</property>
1704                                             <child>
1705                                               <object class="GtkLabel" id="label22">
1706                                                 <property name="visible">True</property>
1707                                                 <property name="can_focus">False</property>
1708                                                 <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;e&lt;/sub&gt;)</property>
1709                                                 <property name="use_markup">True</property>
1710                                               </object>
1711                                             </child>
1712                                           </object>
1713                                           <packing>
1714                                             <property name="expand">True</property>
1715                                             <property name="fill">True</property>
1716                                             <property name="position">0</property>
1717                                           </packing>
1718                                         </child>
1719                                         <child>
1720                                           <object class="GtkButton" id="butAnd_elim_left">
1721                                             <property name="visible">True</property>
1722                                             <property name="can_focus">True</property>
1723                                             <property name="receives_default">True</property>
1724                                             <child>
1725                                               <object class="GtkLabel" id="label23">
1726                                                 <property name="visible">True</property>
1727                                                 <property name="can_focus">False</property>
1728                                                 <property name="label" translatable="yes">Conjunction left (∧&lt;sub&gt;e-l&lt;/sub&gt;)</property>
1729                                                 <property name="use_markup">True</property>
1730                                               </object>
1731                                             </child>
1732                                           </object>
1733                                           <packing>
1734                                             <property name="expand">True</property>
1735                                             <property name="fill">True</property>
1736                                             <property name="position">1</property>
1737                                           </packing>
1738                                         </child>
1739                                         <child>
1740                                           <object class="GtkButton" id="butAnd_elim_right">
1741                                             <property name="visible">True</property>
1742                                             <property name="can_focus">True</property>
1743                                             <property name="receives_default">True</property>
1744                                             <child>
1745                                               <object class="GtkLabel" id="label24">
1746                                                 <property name="visible">True</property>
1747                                                 <property name="can_focus">False</property>
1748                                                 <property name="label" translatable="yes">Conjunction right (∧&lt;sub&gt;e-r&lt;/sub&gt;)</property>
1749                                                 <property name="use_markup">True</property>
1750                                               </object>
1751                                             </child>
1752                                           </object>
1753                                           <packing>
1754                                             <property name="expand">True</property>
1755                                             <property name="fill">True</property>
1756                                             <property name="position">2</property>
1757                                           </packing>
1758                                         </child>
1759                                         <child>
1760                                           <object class="GtkButton" id="butOr_elim">
1761                                             <property name="visible">True</property>
1762                                             <property name="can_focus">True</property>
1763                                             <property name="receives_default">True</property>
1764                                             <child>
1765                                               <object class="GtkLabel" id="label27">
1766                                                 <property name="visible">True</property>
1767                                                 <property name="can_focus">False</property>
1768                                                 <property name="label" translatable="yes">Disjunction (∨&lt;sub&gt;e&lt;/sub&gt;)</property>
1769                                                 <property name="use_markup">True</property>
1770                                               </object>
1771                                             </child>
1772                                           </object>
1773                                           <packing>
1774                                             <property name="expand">True</property>
1775                                             <property name="fill">True</property>
1776                                             <property name="position">3</property>
1777                                           </packing>
1778                                         </child>
1779                                         <child>
1780                                           <object class="GtkButton" id="butNot_elim">
1781                                             <property name="visible">True</property>
1782                                             <property name="can_focus">True</property>
1783                                             <property name="receives_default">True</property>
1784                                             <child>
1785                                               <object class="GtkLabel" id="label31">
1786                                                 <property name="visible">True</property>
1787                                                 <property name="can_focus">False</property>
1788                                                 <property name="label" translatable="yes">Negation (¬&lt;sub&gt;e&lt;/sub&gt;)</property>
1789                                                 <property name="use_markup">True</property>
1790                                               </object>
1791                                             </child>
1792                                           </object>
1793                                           <packing>
1794                                             <property name="expand">True</property>
1795                                             <property name="fill">True</property>
1796                                             <property name="position">4</property>
1797                                           </packing>
1798                                         </child>
1799                                         <child>
1800                                           <object class="GtkButton" id="butBot_elim">
1801                                             <property name="visible">True</property>
1802                                             <property name="can_focus">True</property>
1803                                             <property name="receives_default">True</property>
1804                                             <child>
1805                                               <object class="GtkLabel" id="label33">
1806                                                 <property name="visible">True</property>
1807                                                 <property name="can_focus">False</property>
1808                                                 <property name="label" translatable="yes">Bottom (⊥&lt;sub&gt;e&lt;/sub&gt;)</property>
1809                                                 <property name="use_markup">True</property>
1810                                               </object>
1811                                             </child>
1812                                           </object>
1813                                           <packing>
1814                                             <property name="expand">True</property>
1815                                             <property name="fill">True</property>
1816                                             <property name="position">5</property>
1817                                           </packing>
1818                                         </child>
1819                                         <child>
1820                                           <object class="GtkButton" id="butForall_elim">
1821                                             <property name="visible">True</property>
1822                                             <property name="can_focus">True</property>
1823                                             <property name="receives_default">True</property>
1824                                             <child>
1825                                               <object class="GtkLabel" id="label34">
1826                                                 <property name="visible">True</property>
1827                                                 <property name="can_focus">False</property>
1828                                                 <property name="label" translatable="yes">Universal (∀&lt;sub&gt;e&lt;/sub&gt;)</property>
1829                                                 <property name="use_markup">True</property>
1830                                               </object>
1831                                             </child>
1832                                           </object>
1833                                           <packing>
1834                                             <property name="expand">True</property>
1835                                             <property name="fill">True</property>
1836                                             <property name="position">6</property>
1837                                           </packing>
1838                                         </child>
1839                                         <child>
1840                                           <object class="GtkButton" id="butExists_elim">
1841                                             <property name="visible">True</property>
1842                                             <property name="can_focus">True</property>
1843                                             <property name="receives_default">True</property>
1844                                             <child>
1845                                               <object class="GtkLabel" id="label35">
1846                                                 <property name="visible">True</property>
1847                                                 <property name="can_focus">False</property>
1848                                                 <property name="label" translatable="yes">Existential (∃&lt;sub&gt;e&lt;/sub&gt;)</property>
1849                                                 <property name="use_markup">True</property>
1850                                               </object>
1851                                             </child>
1852                                           </object>
1853                                           <packing>
1854                                             <property name="expand">True</property>
1855                                             <property name="fill">True</property>
1856                                             <property name="position">7</property>
1857                                           </packing>
1858                                         </child>
1859                                       </object>
1860                                     </child>
1861                                     <child type="label">
1862                                       <object class="GtkLabel" id="label5">
1863                                         <property name="visible">True</property>
1864                                         <property name="can_focus">False</property>
1865                                         <property name="label" translatable="yes">Elimination rules</property>
1866                                       </object>
1867                                     </child>
1868                                   </object>
1869                                   <packing>
1870                                     <property name="expand">False</property>
1871                                     <property name="fill">True</property>
1872                                     <property name="position">1</property>
1873                                   </packing>
1874                                 </child>
1875                                 <child>
1876                                   <object class="GtkExpander" id="expander3">
1877                                     <property name="visible">True</property>
1878                                     <property name="can_focus">True</property>
1879                                     <child>
1880                                       <object class="GtkBox" id="vbox4">
1881                                         <property name="visible">True</property>
1882                                         <property name="can_focus">False</property>
1883                                         <property name="orientation">vertical</property>
1884                                         <child>
1885                                           <object class="GtkButton" id="butRAA">
1886                                             <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
1887                                             <property name="visible">True</property>
1888                                             <property name="can_focus">True</property>
1889                                             <property name="receives_default">True</property>
1890                                           </object>
1891                                           <packing>
1892                                             <property name="expand">True</property>
1893                                             <property name="fill">True</property>
1894                                             <property name="position">0</property>
1895                                           </packing>
1896                                         </child>
1897                                         <child>
1898                                           <object class="GtkButton" id="butUseLemma">
1899                                             <property name="label" translatable="yes">Use lemma (lem)</property>
1900                                             <property name="visible">True</property>
1901                                             <property name="can_focus">True</property>
1902                                             <property name="receives_default">True</property>
1903                                           </object>
1904                                           <packing>
1905                                             <property name="expand">True</property>
1906                                             <property name="fill">True</property>
1907                                             <property name="position">1</property>
1908                                           </packing>
1909                                         </child>
1910                                         <child>
1911                                           <object class="GtkButton" id="butDischarge">
1912                                             <property name="label" translatable="yes">Discharge (discharge)</property>
1913                                             <property name="visible">True</property>
1914                                             <property name="can_focus">True</property>
1915                                             <property name="receives_default">True</property>
1916                                           </object>
1917                                           <packing>
1918                                             <property name="expand">True</property>
1919                                             <property name="fill">True</property>
1920                                             <property name="position">2</property>
1921                                           </packing>
1922                                         </child>
1923                                       </object>
1924                                     </child>
1925                                     <child type="label">
1926                                       <object class="GtkLabel" id="label6">
1927                                         <property name="visible">True</property>
1928                                         <property name="can_focus">False</property>
1929                                         <property name="label" translatable="yes">Misc rules</property>
1930                                       </object>
1931                                     </child>
1932                                   </object>
1933                                   <packing>
1934                                     <property name="expand">False</property>
1935                                     <property name="fill">True</property>
1936                                     <property name="position">2</property>
1937                                   </packing>
1938                                 </child>
1939                               </object>
1940                               <packing>
1941                                 <property name="expand">False</property>
1942                                 <property name="fill">True</property>
1943                                 <property name="position">0</property>
1944                               </packing>
1945                             </child>
1946                           </object>
1947                           <packing>
1948                             <property name="expand">False</property>
1949                             <property name="fill">True</property>
1950                             <property name="position">0</property>
1951                           </packing>
1952                         </child>
1953                         <child>
1954                           <object class="GtkBox" id="vboxScript">
1955                             <property name="width_request">400</property>
1956                             <property name="visible">True</property>
1957                             <property name="can_focus">False</property>
1958                             <property name="orientation">vertical</property>
1959                             <child>
1960                               <object class="GtkBox" id="hbox28">
1961                                 <property name="visible">True</property>
1962                                 <property name="can_focus">False</property>
1963                                 <child>
1964                                   <object class="GtkToolbar" id="buttonsToolbar">
1965                                     <property name="visible">True</property>
1966                                     <property name="can_focus">False</property>
1967                                     <property name="toolbar_style">both</property>
1968                                     <child>
1969                                       <object class="GtkToolItem" id="toolitem41">
1970                                         <property name="visible">True</property>
1971                                         <property name="can_focus">False</property>
1972                                         <child>
1973                                           <object class="GtkButton" id="scriptTopButton">
1974                                             <property name="visible">True</property>
1975                                             <property name="can_focus">True</property>
1976                                             <property name="receives_default">False</property>
1977                                             <property name="tooltip_text" translatable="yes">Retract all</property>
1978                                             <property name="relief">none</property>
1979                                             <child>
1980                                               <object class="GtkImage" id="image920">
1981                                                 <property name="visible">True</property>
1982                                                 <property name="can_focus">False</property>
1983                                                 <property name="stock">gtk-goto-top</property>
1984                                               </object>
1985                                             </child>
1986                                           </object>
1987                                         </child>
1988                                       </object>
1989                                       <packing>
1990                                         <property name="expand">False</property>
1991                                         <property name="homogeneous">False</property>
1992                                       </packing>
1993                                     </child>
1994                                     <child>
1995                                       <object class="GtkToolItem" id="toolitem42">
1996                                         <property name="visible">True</property>
1997                                         <property name="can_focus">False</property>
1998                                         <child>
1999                                           <object class="GtkButton" id="scriptRetractButton">
2000                                             <property name="visible">True</property>
2001                                             <property name="can_focus">True</property>
2002                                             <property name="receives_default">False</property>
2003                                             <property name="tooltip_text" translatable="yes">Retract 1 phrase</property>
2004                                             <property name="relief">none</property>
2005                                             <child>
2006                                               <object class="GtkImage" id="image921">
2007                                                 <property name="visible">True</property>
2008                                                 <property name="can_focus">False</property>
2009                                                 <property name="stock">gtk-go-up</property>
2010                                               </object>
2011                                             </child>
2012                                           </object>
2013                                         </child>
2014                                       </object>
2015                                       <packing>
2016                                         <property name="expand">False</property>
2017                                         <property name="homogeneous">False</property>
2018                                       </packing>
2019                                     </child>
2020                                     <child>
2021                                       <object class="GtkToolItem" id="toolitem43">
2022                                         <property name="visible">True</property>
2023                                         <property name="can_focus">False</property>
2024                                         <child>
2025                                           <object class="GtkButton" id="scriptJumpButton">
2026                                             <property name="visible">True</property>
2027                                             <property name="can_focus">True</property>
2028                                             <property name="receives_default">False</property>
2029                                             <property name="tooltip_text" translatable="yes">Execute until cursor</property>
2030                                             <property name="relief">none</property>
2031                                             <child>
2032                                               <object class="GtkImage" id="image922">
2033                                                 <property name="visible">True</property>
2034                                                 <property name="can_focus">False</property>
2035                                                 <property name="stock">gtk-jump-to</property>
2036                                               </object>
2037                                             </child>
2038                                           </object>
2039                                         </child>
2040                                       </object>
2041                                       <packing>
2042                                         <property name="expand">False</property>
2043                                         <property name="homogeneous">False</property>
2044                                       </packing>
2045                                     </child>
2046                                     <child>
2047                                       <object class="GtkToolItem" id="toolitem44">
2048                                         <property name="visible">True</property>
2049                                         <property name="can_focus">False</property>
2050                                         <child>
2051                                           <object class="GtkButton" id="scriptAdvanceButton">
2052                                             <property name="visible">True</property>
2053                                             <property name="can_focus">True</property>
2054                                             <property name="receives_default">False</property>
2055                                             <property name="tooltip_text" translatable="yes">Execute 1 phrase</property>
2056                                             <property name="relief">none</property>
2057                                             <child>
2058                                               <object class="GtkImage" id="image923">
2059                                                 <property name="visible">True</property>
2060                                                 <property name="can_focus">False</property>
2061                                                 <property name="stock">gtk-go-down</property>
2062                                               </object>
2063                                             </child>
2064                                           </object>
2065                                         </child>
2066                                       </object>
2067                                       <packing>
2068                                         <property name="expand">False</property>
2069                                         <property name="homogeneous">False</property>
2070                                       </packing>
2071                                     </child>
2072                                     <child>
2073                                       <object class="GtkToolItem" id="toolitem45">
2074                                         <property name="visible">True</property>
2075                                         <property name="can_focus">False</property>
2076                                         <child>
2077                                           <object class="GtkButton" id="scriptBottomButton">
2078                                             <property name="visible">True</property>
2079                                             <property name="can_focus">True</property>
2080                                             <property name="receives_default">False</property>
2081                                             <property name="tooltip_text" translatable="yes">Execute all</property>
2082                                             <property name="relief">none</property>
2083                                             <child>
2084                                               <object class="GtkImage" id="image924">
2085                                                 <property name="visible">True</property>
2086                                                 <property name="can_focus">False</property>
2087                                                 <property name="stock">gtk-goto-bottom</property>
2088                                               </object>
2089                                             </child>
2090                                           </object>
2091                                         </child>
2092                                       </object>
2093                                       <packing>
2094                                         <property name="expand">False</property>
2095                                         <property name="homogeneous">False</property>
2096                                       </packing>
2097                                     </child>
2098                                   </object>
2099                                   <packing>
2100                                     <property name="expand">True</property>
2101                                     <property name="fill">True</property>
2102                                     <property name="position">0</property>
2103                                   </packing>
2104                                 </child>
2105                                 <child>
2106                                   <object class="GtkToolbar" id="toolbar2">
2107                                     <property name="visible">True</property>
2108                                     <property name="can_focus">False</property>
2109                                     <property name="orientation">vertical</property>
2110                                     <property name="toolbar_style">both</property>
2111                                     <child>
2112                                       <object class="GtkToolItem" id="toolitem46">
2113                                         <property name="visible">True</property>
2114                                         <property name="can_focus">False</property>
2115                                         <child>
2116                                           <object class="GtkButton" id="scriptAbortButton">
2117                                             <property name="visible">True</property>
2118                                             <property name="can_focus">True</property>
2119                                             <property name="receives_default">False</property>
2120                                             <property name="relief">none</property>
2121                                             <child>
2122                                               <object class="GtkImage" id="image927">
2123                                                 <property name="visible">True</property>
2124                                                 <property name="can_focus">False</property>
2125                                                 <property name="stock">gtk-stop</property>
2126                                               </object>
2127                                             </child>
2128                                           </object>
2129                                         </child>
2130                                       </object>
2131                                       <packing>
2132                                         <property name="expand">False</property>
2133                                         <property name="homogeneous">False</property>
2134                                       </packing>
2135                                     </child>
2136                                   </object>
2137                                   <packing>
2138                                     <property name="expand">False</property>
2139                                     <property name="fill">True</property>
2140                                     <property name="position">1</property>
2141                                   </packing>
2142                                 </child>
2143                               </object>
2144                               <packing>
2145                                 <property name="expand">False</property>
2146                                 <property name="fill">False</property>
2147                                 <property name="position">0</property>
2148                               </packing>
2149                             </child>
2150                             <child>
2151                               <object class="GtkNotebook" id="scriptNotebook">
2152                                 <property name="visible">True</property>
2153                                 <property name="can_focus">True</property>
2154                                 <property name="scrollable">True</property>
2155                               </object>
2156                               <packing>
2157                                 <property name="expand">True</property>
2158                                 <property name="fill">True</property>
2159                                 <property name="position">1</property>
2160                               </packing>
2161                             </child>
2162                           </object>
2163                           <packing>
2164                             <property name="expand">True</property>
2165                             <property name="fill">True</property>
2166                             <property name="position">1</property>
2167                           </packing>
2168                         </child>
2169                       </object>
2170                       <packing>
2171                         <property name="resize">False</property>
2172                         <property name="shrink">True</property>
2173                       </packing>
2174                     </child>
2175                     <child>
2176                       <object class="GtkPaned" id="vpaned1">
2177                         <property name="width_request">250</property>
2178                         <property name="height_request">500</property>
2179                         <property name="visible">True</property>
2180                         <property name="can_focus">True</property>
2181                         <property name="orientation">vertical</property>
2182                         <property name="position">380</property>
2183                         <child>
2184                           <object class="GtkNotebook" id="sequentsNotebook">
2185                             <property name="visible">True</property>
2186                             <property name="can_focus">True</property>
2187                             <property name="scrollable">True</property>
2188                           </object>
2189                           <packing>
2190                             <property name="resize">False</property>
2191                             <property name="shrink">True</property>
2192                           </packing>
2193                         </child>
2194                         <child>
2195                           <object class="GtkBox" id="hbox9">
2196                             <property name="visible">True</property>
2197                             <property name="can_focus">False</property>
2198                             <child>
2199                               <object class="GtkScrolledWindow" id="logScrolledWin">
2200                                 <property name="visible">True</property>
2201                                 <property name="can_focus">True</property>
2202                                 <property name="hscrollbar_policy">never</property>
2203                                 <property name="shadow_type">in</property>
2204                                 <child>
2205                                   <object class="GtkTextView" id="logTextView">
2206                                     <property name="visible">True</property>
2207                                     <property name="can_focus">True</property>
2208                                     <property name="editable">False</property>
2209                                     <property name="wrap_mode">char</property>
2210                                     <property name="cursor_visible">False</property>
2211                                   </object>
2212                                 </child>
2213                               </object>
2214                               <packing>
2215                                 <property name="expand">True</property>
2216                                 <property name="fill">True</property>
2217                                 <property name="position">0</property>
2218                               </packing>
2219                             </child>
2220                           </object>
2221                           <packing>
2222                             <property name="resize">True</property>
2223                             <property name="shrink">True</property>
2224                           </packing>
2225                         </child>
2226                       </object>
2227                       <packing>
2228                         <property name="resize">True</property>
2229                         <property name="shrink">True</property>
2230                       </packing>
2231                     </child>
2232                   </object>
2233                   <packing>
2234                     <property name="expand">True</property>
2235                     <property name="fill">True</property>
2236                     <property name="position">0</property>
2237                   </packing>
2238                 </child>
2239               </object>
2240               <packing>
2241                 <property name="expand">True</property>
2242                 <property name="fill">True</property>
2243                 <property name="position">1</property>
2244               </packing>
2245             </child>
2246             <child>
2247               <object class="GtkBox" id="hbox10">
2248                 <property name="visible">True</property>
2249                 <property name="can_focus">False</property>
2250                 <child>
2251                   <object class="GtkStatusbar" id="StatusBar">
2252                     <property name="visible">True</property>
2253                     <property name="can_focus">False</property>
2254                   </object>
2255                   <packing>
2256                     <property name="expand">True</property>
2257                     <property name="fill">True</property>
2258                     <property name="position">0</property>
2259                   </packing>
2260                 </child>
2261                 <child>
2262                   <object class="GtkNotebook" id="HintNotebook">
2263                     <property name="visible">True</property>
2264                     <property name="can_focus">False</property>
2265                     <property name="show_tabs">False</property>
2266                     <child>
2267                       <object class="GtkImage" id="HintLowImage">
2268                         <property name="visible">True</property>
2269                         <property name="can_focus">False</property>
2270                         <property name="stock">gtk-missing-image</property>
2271                       </object>
2272                     </child>
2273                     <child type="tab">
2274                       <object class="GtkLabel" id="label14">
2275                         <property name="visible">True</property>
2276                         <property name="can_focus">False</property>
2277                         <property name="label" translatable="yes">label14</property>
2278                       </object>
2279                       <packing>
2280                         <property name="tab_fill">False</property>
2281                       </packing>
2282                     </child>
2283                     <child>
2284                       <object class="GtkImage" id="HintMediumImage">
2285                         <property name="visible">True</property>
2286                         <property name="can_focus">False</property>
2287                         <property name="stock">gtk-missing-image</property>
2288                       </object>
2289                       <packing>
2290                         <property name="position">1</property>
2291                       </packing>
2292                     </child>
2293                     <child type="tab">
2294                       <object class="GtkLabel" id="label15">
2295                         <property name="visible">True</property>
2296                         <property name="can_focus">False</property>
2297                         <property name="label" translatable="yes">label15</property>
2298                       </object>
2299                       <packing>
2300                         <property name="position">1</property>
2301                         <property name="tab_fill">False</property>
2302                       </packing>
2303                     </child>
2304                     <child>
2305                       <object class="GtkImage" id="HintHighImage">
2306                         <property name="visible">True</property>
2307                         <property name="can_focus">False</property>
2308                         <property name="stock">gtk-missing-image</property>
2309                       </object>
2310                       <packing>
2311                         <property name="position">2</property>
2312                       </packing>
2313                     </child>
2314                     <child type="tab">
2315                       <object class="GtkLabel" id="label16">
2316                         <property name="visible">True</property>
2317                         <property name="can_focus">False</property>
2318                         <property name="label" translatable="yes">label16</property>
2319                       </object>
2320                       <packing>
2321                         <property name="position">2</property>
2322                         <property name="tab_fill">False</property>
2323                       </packing>
2324                     </child>
2325                   </object>
2326                   <packing>
2327                     <property name="expand">False</property>
2328                     <property name="fill">True</property>
2329                     <property name="position">1</property>
2330                   </packing>
2331                 </child>
2332               </object>
2333               <packing>
2334                 <property name="expand">False</property>
2335                 <property name="fill">False</property>
2336                 <property name="position">2</property>
2337               </packing>
2338             </child>
2339           </object>
2340         </child>
2341       </object>
2342     </child>
2343   </object>
2344   <object class="GtkDialog" id="UriChoiceDialog">
2345     <property name="height_request">280</property>
2346     <property name="can_focus">False</property>
2347     <property name="title" translatable="yes">Uri choice</property>
2348     <property name="modal">True</property>
2349     <property name="window_position">center</property>
2350     <property name="type_hint">dialog</property>
2351     <child internal-child="vbox">
2352       <object class="GtkBox" id="dialog-vbox3">
2353         <property name="visible">True</property>
2354         <property name="can_focus">False</property>
2355         <property name="orientation">vertical</property>
2356         <property name="spacing">4</property>
2357         <child internal-child="action_area">
2358           <object class="GtkButtonBox" id="dialog-action_area3">
2359             <property name="visible">True</property>
2360             <property name="can_focus">False</property>
2361             <property name="layout_style">end</property>
2362             <child>
2363               <object class="GtkButton" id="UriChoiceAbortButton">
2364                 <property name="label">gtk-cancel</property>
2365                 <property name="visible">True</property>
2366                 <property name="can_focus">True</property>
2367                 <property name="can_default">True</property>
2368                 <property name="receives_default">False</property>
2369                 <property name="use_stock">True</property>
2370               </object>
2371               <packing>
2372                 <property name="expand">False</property>
2373                 <property name="fill">False</property>
2374                 <property name="position">0</property>
2375               </packing>
2376             </child>
2377             <child>
2378               <object class="GtkButton" id="UriChoiceSelectedButton">
2379                 <property name="visible">True</property>
2380                 <property name="can_focus">True</property>
2381                 <property name="can_default">True</property>
2382                 <property name="receives_default">False</property>
2383                 <child>
2384                   <object class="GtkAlignment" id="alignment2">
2385                     <property name="visible">True</property>
2386                     <property name="can_focus">False</property>
2387                     <property name="xscale">0</property>
2388                     <property name="yscale">0</property>
2389                     <child>
2390                       <object class="GtkBox" id="hbox3">
2391                         <property name="visible">True</property>
2392                         <property name="can_focus">False</property>
2393                         <property name="spacing">2</property>
2394                         <child>
2395                           <object class="GtkImage" id="image19">
2396                             <property name="visible">True</property>
2397                             <property name="can_focus">False</property>
2398                             <property name="stock">gtk-index</property>
2399                           </object>
2400                           <packing>
2401                             <property name="expand">False</property>
2402                             <property name="fill">False</property>
2403                             <property name="position">0</property>
2404                           </packing>
2405                         </child>
2406                         <child>
2407                           <object class="GtkLabel" id="label3">
2408                             <property name="visible">True</property>
2409                             <property name="can_focus">False</property>
2410                             <property name="label" translatable="yes">Try _Selected</property>
2411                             <property name="use_underline">True</property>
2412                           </object>
2413                           <packing>
2414                             <property name="expand">False</property>
2415                             <property name="fill">False</property>
2416                             <property name="position">1</property>
2417                           </packing>
2418                         </child>
2419                       </object>
2420                     </child>
2421                   </object>
2422                 </child>
2423               </object>
2424               <packing>
2425                 <property name="expand">False</property>
2426                 <property name="fill">False</property>
2427                 <property name="position">1</property>
2428               </packing>
2429             </child>
2430             <child>
2431               <object class="GtkButton" id="UriChoiceConstantsButton">
2432                 <property name="label" translatable="yes">Try Constants</property>
2433                 <property name="visible">True</property>
2434                 <property name="sensitive">False</property>
2435                 <property name="can_focus">True</property>
2436                 <property name="can_default">True</property>
2437                 <property name="receives_default">False</property>
2438                 <property name="use_underline">True</property>
2439               </object>
2440               <packing>
2441                 <property name="expand">False</property>
2442                 <property name="fill">False</property>
2443                 <property name="position">2</property>
2444               </packing>
2445             </child>
2446             <child>
2447               <object class="GtkButton" id="copyButton">
2448                 <property name="label">gtk-copy</property>
2449                 <property name="can_focus">True</property>
2450                 <property name="can_default">True</property>
2451                 <property name="receives_default">False</property>
2452                 <property name="use_stock">True</property>
2453               </object>
2454               <packing>
2455                 <property name="expand">False</property>
2456                 <property name="fill">False</property>
2457                 <property name="position">3</property>
2458               </packing>
2459             </child>
2460             <child>
2461               <object class="GtkButton" id="uriChoiceAutoButton">
2462                 <property name="visible">True</property>
2463                 <property name="can_focus">True</property>
2464                 <property name="can_default">True</property>
2465                 <property name="receives_default">False</property>
2466                 <child>
2467                   <object class="GtkAlignment" id="alignment5">
2468                     <property name="visible">True</property>
2469                     <property name="can_focus">False</property>
2470                     <property name="xscale">0</property>
2471                     <property name="yscale">0</property>
2472                     <child>
2473                       <object class="GtkBox" id="hbox16">
2474                         <property name="visible">True</property>
2475                         <property name="can_focus">False</property>
2476                         <property name="spacing">2</property>
2477                         <child>
2478                           <object class="GtkImage" id="image302">
2479                             <property name="visible">True</property>
2480                             <property name="can_focus">False</property>
2481                             <property name="stock">gtk-ok</property>
2482                           </object>
2483                           <packing>
2484                             <property name="expand">False</property>
2485                             <property name="fill">False</property>
2486                             <property name="position">0</property>
2487                           </packing>
2488                         </child>
2489                         <child>
2490                           <object class="GtkLabel" id="okLabel">
2491                             <property name="visible">True</property>
2492                             <property name="can_focus">False</property>
2493                             <property name="label" translatable="yes">bla bla bla</property>
2494                             <property name="use_underline">True</property>
2495                           </object>
2496                           <packing>
2497                             <property name="expand">False</property>
2498                             <property name="fill">False</property>
2499                             <property name="position">1</property>
2500                           </packing>
2501                         </child>
2502                       </object>
2503                     </child>
2504                   </object>
2505                 </child>
2506               </object>
2507               <packing>
2508                 <property name="expand">False</property>
2509                 <property name="fill">False</property>
2510                 <property name="position">4</property>
2511               </packing>
2512             </child>
2513             <child>
2514               <object class="GtkButton" id="uriChoiceForwardButton">
2515                 <property name="label">gtk-go-forward</property>
2516                 <property name="visible">True</property>
2517                 <property name="can_focus">True</property>
2518                 <property name="can_default">True</property>
2519                 <property name="receives_default">False</property>
2520                 <property name="use_stock">True</property>
2521               </object>
2522               <packing>
2523                 <property name="expand">False</property>
2524                 <property name="fill">False</property>
2525                 <property name="position">5</property>
2526               </packing>
2527             </child>
2528           </object>
2529           <packing>
2530             <property name="expand">False</property>
2531             <property name="fill">False</property>
2532             <property name="pack_type">end</property>
2533             <property name="position">0</property>
2534           </packing>
2535         </child>
2536         <child>
2537           <object class="GtkBox" id="vbox2">
2538             <property name="visible">True</property>
2539             <property name="can_focus">False</property>
2540             <property name="orientation">vertical</property>
2541             <property name="spacing">3</property>
2542             <child>
2543               <object class="GtkLabel" id="UriChoiceLabel">
2544                 <property name="visible">True</property>
2545                 <property name="can_focus">False</property>
2546                 <property name="label" translatable="yes">some informative message here ...</property>
2547               </object>
2548               <packing>
2549                 <property name="expand">False</property>
2550                 <property name="fill">False</property>
2551                 <property name="position">0</property>
2552               </packing>
2553             </child>
2554             <child>
2555               <object class="GtkScrolledWindow" id="scrolledwindow1">
2556                 <property name="width_request">400</property>
2557                 <property name="visible">True</property>
2558                 <property name="can_focus">True</property>
2559                 <property name="vexpand">True</property>
2560                 <child>
2561                   <object class="GtkTreeView" id="UriChoiceTreeView">
2562                     <property name="visible">True</property>
2563                     <property name="can_focus">True</property>
2564                     <property name="headers_visible">False</property>
2565                     <child internal-child="selection">
2566                       <object class="GtkTreeSelection"/>
2567                     </child>
2568                   </object>
2569                 </child>
2570               </object>
2571               <packing>
2572                 <property name="expand">True</property>
2573                 <property name="fill">True</property>
2574                 <property name="position">1</property>
2575               </packing>
2576             </child>
2577             <child>
2578               <object class="GtkBox" id="uriEntryHBox">
2579                 <property name="visible">True</property>
2580                 <property name="can_focus">False</property>
2581                 <property name="vexpand">True</property>
2582                 <child>
2583                   <object class="GtkLabel" id="label2">
2584                     <property name="visible">True</property>
2585                     <property name="can_focus">False</property>
2586                     <property name="label" translatable="yes">URI: </property>
2587                   </object>
2588                   <packing>
2589                     <property name="expand">False</property>
2590                     <property name="fill">False</property>
2591                     <property name="position">0</property>
2592                   </packing>
2593                 </child>
2594                 <child>
2595                   <object class="GtkEntry" id="entry1">
2596                     <property name="visible">True</property>
2597                     <property name="can_focus">True</property>
2598                   </object>
2599                   <packing>
2600                     <property name="expand">True</property>
2601                     <property name="fill">True</property>
2602                     <property name="position">1</property>
2603                   </packing>
2604                 </child>
2605               </object>
2606               <packing>
2607                 <property name="expand">True</property>
2608                 <property name="fill">True</property>
2609                 <property name="position">2</property>
2610               </packing>
2611             </child>
2612           </object>
2613           <packing>
2614             <property name="expand">False</property>
2615             <property name="fill">True</property>
2616             <property name="position">2</property>
2617           </packing>
2618         </child>
2619       </object>
2620     </child>
2621     <action-widgets>
2622       <action-widget response="-6">UriChoiceAbortButton</action-widget>
2623     </action-widgets>
2624   </object>
2625 </interface>