helm/software/matita/matita.glade

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