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