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                             <child>
 774                               <widget class="GtkImageMenuItem" id="developmentsMenuItem">
 775                                 <property name="visible">True</property>
 776                                 <property name="label" translatable="yes">_Developments...</property>
 777                                 <property name="use_underline">True</property>
 778                                 <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 779                                 <child internal-child="image">
 780                                   <widget class="GtkImage" id="image1051">
 781                                     <property name="visible">True</property>
 782                                     <property name="stock">gtk-execute</property>
 783                                     <property name="icon_size">1</property>
 784                                   </widget>
 785                                 </child>
 786                               </widget>
 787                             </child>
 788                             <child>
 789                               <widget class="GtkSeparatorMenuItem" id="separator2">
 790                                 <property name="visible">True</property>
 791                               </widget>
 792                             </child>
 793                             <child>
 794                               <widget class="GtkImageMenuItem" id="quitMenuItem">
 795                                 <property name="visible">True</property>
 796                                 <property name="label" translatable="yes">_Quit</property>
 797                                 <property name="use_underline">True</property>
 798                                 <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 799                                 <child internal-child="image">
 800                                   <widget class="GtkImage" id="image1052">
 801                                     <property name="visible">True</property>
 802                                     <property name="stock">gtk-quit</property>
 803                                     <property name="icon_size">1</property>
 804                                   </widget>
 805                                 </child>
 806                               </widget>
 807                             </child>
 808                           </widget>
 809                         </child>
 810                       </widget>
 811                     </child>
 812                     <child>
 813                       <widget class="GtkMenuItem" id="editMenu">
 814                         <property name="visible">True</property>
 815                         <property name="label" translatable="yes">_Edit</property>
 816                         <property name="use_underline">True</property>
 817                         <child>
 818                           <widget class="GtkMenu" id="editMenu_menu">
 819                             <child>
 820                               <widget class="GtkImageMenuItem" id="undoMenuItem">
 821                                 <property name="visible">True</property>
 822                                 <property name="sensitive">False</property>
 823                                 <property name="label" translatable="yes">_Undo</property>
 824                                 <property name="use_underline">True</property>
 825                                 <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 826                                 <child internal-child="image">
 827                                   <widget class="GtkImage" id="image1053">
 828                                     <property name="visible">True</property>
 829                                     <property name="stock">gtk-undo</property>
 830                                     <property name="icon_size">1</property>
 831                                   </widget>
 832                                 </child>
 833                               </widget>
 834                             </child>
 835                             <child>
 836                               <widget class="GtkImageMenuItem" id="redoMenuItem">
 837                                 <property name="visible">True</property>
 838                                 <property name="sensitive">False</property>
 839                                 <property name="label" translatable="yes">_Redo</property>
 840                                 <property name="use_underline">True</property>
 841                                 <accelerator key="z" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK" signal="activate"/>
 842                                 <child internal-child="image">
 843                                   <widget class="GtkImage" id="image1054">
 844                                     <property name="visible">True</property>
 845                                     <property name="stock">gtk-redo</property>
 846                                     <property name="icon_size">1</property>
 847                                   </widget>
 848                                 </child>
 849                               </widget>
 850                             </child>
 851                             <child>
 852                               <widget class="GtkSeparatorMenuItem" id="separator3">
 853                                 <property name="visible">True</property>
 854                               </widget>
 855                             </child>
 856                             <child>
 857                               <widget class="GtkImageMenuItem" id="cutMenuItem">
 858                                 <property name="visible">True</property>
 859                                 <property name="label" translatable="yes">Cu_t</property>
 860                                 <property name="use_underline">True</property>
 861                                 <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 862                                 <child internal-child="image">
 863                                   <widget class="GtkImage" id="image1055">
 864                                     <property name="visible">True</property>
 865                                     <property name="stock">gtk-cut</property>
 866                                     <property name="icon_size">1</property>
 867                                   </widget>
 868                                 </child>
 869                               </widget>
 870                             </child>
 871                             <child>
 872                               <widget class="GtkImageMenuItem" id="copyMenuItem">
 873                                 <property name="visible">True</property>
 874                                 <property name="label" translatable="yes">_Copy</property>
 875                                 <property name="use_underline">True</property>
 876                                 <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 877                                 <child internal-child="image">
 878                                   <widget class="GtkImage" id="image1056">
 879                                     <property name="visible">True</property>
 880                                     <property name="stock">gtk-copy</property>
 881                                     <property name="icon_size">1</property>
 882                                   </widget>
 883                                 </child>
 884                               </widget>
 885                             </child>
 886                             <child>
 887                               <widget class="GtkImageMenuItem" id="pasteMenuItem">
 888                                 <property name="visible">True</property>
 889                                 <property name="label" translatable="yes">_Paste</property>
 890                                 <property name="use_underline">True</property>
 891                                 <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 892                                 <child internal-child="image">
 893                                   <widget class="GtkImage" id="image1057">
 894                                     <property name="visible">True</property>
 895                                     <property name="stock">gtk-paste</property>
 896                                     <property name="icon_size">1</property>
 897                                   </widget>
 898                                 </child>
 899                               </widget>
 900                             </child>
 901                             <child>
 902                               <widget class="GtkMenuItem" id="pastePatternMenuItem">
 903                                 <property name="visible">True</property>
 904                                 <property name="label" translatable="yes">Paste as pattern</property>
 905                                 <property name="use_underline">True</property>
 906                               </widget>
 907                             </child>
 908                             <child>
 909                               <widget class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
 910                                 <property name="visible">True</property>
 911                                 <property name="label" translatable="yes">Paste Unicode as TeX</property>
 912                                 <property name="use_underline">True</property>
 913                                 <property name="active">False</property>
 914                               </widget>
 915                             </child>
 916                             <child>
 917                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
 918                                 <property name="visible">True</property>
 919                                 <property name="label" translatable="yes">_Delete</property>
 920                                 <property name="use_underline">True</property>
 921                                 <child internal-child="image">
 922                                   <widget class="GtkImage" id="image1058">
 923                                     <property name="visible">True</property>
 924                                     <property name="stock">gtk-delete</property>
 925                                     <property name="icon_size">1</property>
 926                                   </widget>
 927                                 </child>
 928                               </widget>
 929                             </child>
 930                             <child>
 931                               <widget class="GtkSeparatorMenuItem" id="separator4">
 932                                 <property name="visible">True</property>
 933                               </widget>
 934                             </child>
 935                             <child>
 936                               <widget class="GtkMenuItem" id="selectAllMenuItem">
 937                                 <property name="visible">True</property>
 938                                 <property name="label" translatable="yes">Select _All</property>
 939                                 <property name="use_underline">True</property>
 940                               </widget>
 941                             </child>
 942                             <child>
 943                               <widget class="GtkSeparatorMenuItem" id="separator7">
 944                                 <property name="visible">True</property>
 945                               </widget>
 946                             </child>
 947                             <child>
 948                               <widget class="GtkImageMenuItem" id="findReplMenuItem">
 949                                 <property name="visible">True</property>
 950                                 <property name="label" translatable="yes">_Find &amp; replace ...</property>
 951                                 <property name="use_underline">True</property>
 952                                 <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 953                                 <child internal-child="image">
 954                                   <widget class="GtkImage" id="image1059">
 955                                     <property name="visible">True</property>
 956                                     <property name="stock">gtk-find-and-replace</property>
 957                                     <property name="icon_size">1</property>
 958                                   </widget>
 959                                 </child>
 960                               </widget>
 961                             </child>
 962                             <child>
 963                               <widget class="GtkSeparatorMenuItem" id="separator8">
 964                                 <property name="visible">True</property>
 965                               </widget>
 966                             </child>
 967                             <child>
 968                               <widget class="GtkMenuItem" id="LigatureButton">
 969                                 <property name="visible">True</property>
 970                                 <property name="label" translatable="yes">Next ligature</property>
 971                                 <property name="use_underline">True</property>
 972                                 <accelerator key="l" modifiers="GDK_MOD1_MASK" signal="activate"/>
 973                               </widget>
 974                             </child>
 975                             <child>
 976                               <widget class="GtkMenuItem" id="externalEditorMenuItem">
 977                                 <property name="visible">True</property>
 978                                 <property name="label" translatable="yes">Edit with e_xternal editor</property>
 979                                 <property name="use_underline">True</property>
 980                               </widget>
 981                             </child>
 982                           </widget>
 983                         </child>
 984                       </widget>
 985                     </child>
 986                     <child>
 987                       <widget class="GtkMenuItem" id="scriptMenu">
 988                         <property name="visible">True</property>
 989                         <property name="label" translatable="yes">_Script</property>
 990                         <property name="use_underline">True</property>
 991                         <child>
 992                           <widget class="GtkMenu" id="scriptMenu_menu">
 993                             <child>
 994                               <widget class="GtkMenuItem" id="scriptAdvanceMenuItem">
 995                                 <property name="visible">True</property>
 996                                 <property name="label" translatable="yes">Execute 1 phrase</property>
 997                                 <property name="use_underline">True</property>
 998                                 <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
 999                               </widget>
1000                             </child>
1001                             <child>
1002                               <widget class="GtkMenuItem" id="scriptRetractMenuItem">
1003                                 <property name="visible">True</property>
1004                                 <property name="label" translatable="yes">Retract 1 phrase</property>
1005                                 <property name="use_underline">True</property>
1006                                 <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1007                               </widget>
1008                             </child>
1009                             <child>
1010                               <widget class="GtkSeparatorMenuItem" id="separator9">
1011                                 <property name="visible">True</property>
1012                               </widget>
1013                             </child>
1014                             <child>
1015                               <widget class="GtkMenuItem" id="scriptBottomMenuItem">
1016                                 <property name="visible">True</property>
1017                                 <property name="label" translatable="yes">Execute all</property>
1018                                 <property name="use_underline">True</property>
1019                                 <accelerator key="End" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1020                               </widget>
1021                             </child>
1022                             <child>
1023                               <widget class="GtkMenuItem" id="scriptTopMenuItem">
1024                                 <property name="visible">True</property>
1025                                 <property name="label" translatable="yes">Restart</property>
1026                                 <property name="use_underline">True</property>
1027                                 <accelerator key="Home" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1028                               </widget>
1029                             </child>
1030                             <child>
1031                               <widget class="GtkSeparatorMenuItem" id="separator10">
1032                                 <property name="visible">True</property>
1033                               </widget>
1034                             </child>
1035                             <child>
1036                               <widget class="GtkMenuItem" id="scriptJumpMenuItem">
1037                                 <property name="visible">True</property>
1038                                 <property name="label" translatable="yes">Execute until cursor</property>
1039                                 <property name="use_underline">True</property>
1040                                 <accelerator key="period" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1041                               </widget>
1042                             </child>
1043                           </widget>
1044                         </child>
1045                       </widget>
1046                     </child>
1047                     <child>
1048                       <widget class="GtkMenuItem" id="viewMenu">
1049                         <property name="visible">True</property>
1050                         <property name="label" translatable="yes">_View</property>
1051                         <property name="use_underline">True</property>
1052                         <child>
1053                           <widget class="GtkMenu" id="viewMenu_menu">
1054                             <child>
1055                               <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
1056                                 <property name="visible">True</property>
1057                                 <property name="label" translatable="yes">Show _tactics bar</property>
1058                                 <property name="use_underline">True</property>
1059                                 <property name="active">True</property>
1060                                 <accelerator key="F2" modifiers="" signal="activate"/>
1061                               </widget>
1062                             </child>
1063                             <child>
1064                               <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1065                                 <property name="visible">True</property>
1066                                 <property name="label" translatable="yes">New CIC _browser</property>
1067                                 <property name="use_underline">True</property>
1068                                 <accelerator key="F3" modifiers="" signal="activate"/>
1069                               </widget>
1070                             </child>
1071                             <child>
1072                               <widget class="GtkSeparatorMenuItem" id="separator5">
1073                                 <property name="visible">True</property>
1074                               </widget>
1075                             </child>
1076                             <child>
1077                               <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1078                                 <property name="visible">True</property>
1079                                 <property name="label" translatable="yes">_Fullscreen</property>
1080                                 <property name="use_underline">True</property>
1081                                 <accelerator key="F11" modifiers="" signal="activate"/>
1082                               </widget>
1083                             </child>
1084                             <child>
1085                               <widget class="GtkSeparatorMenuItem" id="separator1">
1086                                 <property name="visible">True</property>
1087                               </widget>
1088                             </child>
1089                             <child>
1090                               <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
1091                                 <property name="visible">True</property>
1092                                 <property name="label" translatable="yes">Zoom _in</property>
1093                                 <property name="use_underline">True</property>
1094                                 <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1095                                 <child internal-child="image">
1096                                   <widget class="GtkImage" id="image1060">
1097                                     <property name="visible">True</property>
1098                                     <property name="stock">gtk-zoom-in</property>
1099                                     <property name="icon_size">1</property>
1100                                   </widget>
1101                                 </child>
1102                               </widget>
1103                             </child>
1104                             <child>
1105                               <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
1106                                 <property name="visible">True</property>
1107                                 <property name="label" translatable="yes">Zoom _out</property>
1108                                 <property name="use_underline">True</property>
1109                                 <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1110                                 <child internal-child="image">
1111                                   <widget class="GtkImage" id="image1061">
1112                                     <property name="visible">True</property>
1113                                     <property name="stock">gtk-zoom-out</property>
1114                                     <property name="icon_size">1</property>
1115                                   </widget>
1116                                 </child>
1117                               </widget>
1118                             </child>
1119                             <child>
1120                               <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
1121                                 <property name="visible">True</property>
1122                                 <property name="label" translatable="yes">_Normal size</property>
1123                                 <property name="use_underline">True</property>
1124                                 <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1125                                 <child internal-child="image">
1126                                   <widget class="GtkImage" id="image1062">
1127                                     <property name="visible">True</property>
1128                                     <property name="stock">gtk-zoom-100</property>
1129                                     <property name="icon_size">1</property>
1130                                   </widget>
1131                                 </child>
1132                               </widget>
1133                             </child>
1134                             <child>
1135                               <widget class="GtkSeparatorMenuItem" id="separator12">
1136                                 <property name="visible">True</property>
1137                               </widget>
1138                             </child>
1139                             <child>
1140                               <widget class="GtkCheckMenuItem" id="ppNotationMenuItem">
1141                                 <property name="visible">True</property>
1142                                 <property name="label" translatable="yes">Pretty print notation</property>
1143                                 <property name="use_underline">True</property>
1144                                 <property name="active">True</property>
1145                               </widget>
1146                             </child>
1147                             <child>
1148                               <widget class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
1149                                 <property name="visible">True</property>
1150                                 <property name="label" translatable="yes">Hide coercions</property>
1151                                 <property name="use_underline">True</property>
1152                                 <property name="active">True</property>
1153                               </widget>
1154                             </child>
1155                             <child>
1156                               <widget class="GtkSeparatorMenuItem" id="separator13">
1157                                 <property name="visible">True</property>
1158                               </widget>
1159                             </child>
1160                             <child>
1161                               <widget class="GtkMenuItem" id="showCoercionsGraphMenuItem">
1162                                 <property name="visible">True</property>
1163                                 <property name="tooltip" translatable="yes">Displays the graph of coercions</property>
1164                                 <property name="label" translatable="yes">Coercions Graph</property>
1165                                 <property name="use_underline">True</property>
1166                               </widget>
1167                             </child>
1168                             <child>
1169                               <widget class="GtkImageMenuItem" id="showAutoGuiMenuItem">
1170                                 <property name="visible">True</property>
1171                                 <property name="tooltip" translatable="yes">Displays a window helpful to drive automation</property>
1172                                 <property name="label" translatable="yes">Auto GUI</property>
1173                                 <property name="use_underline">True</property>
1174                                 <child internal-child="image">
1175                                   <widget class="GtkImage" id="menu-item-image19">
1176                                     <property name="stock">gtk-media-pause</property>
1177                                   </widget>
1178                                 </child>
1179                               </widget>
1180                             </child>
1181                           </widget>
1182                         </child>
1183                       </widget>
1184                     </child>
1185                     <child>
1186                       <widget class="GtkMenuItem" id="debugMenu">
1187                         <property name="visible">True</property>
1188                         <property name="label" translatable="yes">_Debug</property>
1189                         <property name="use_underline">True</property>
1190                         <child>
1191                           <widget class="GtkMenu" id="debugMenu_menu">
1192                             <child>
1193                               <widget class="GtkSeparatorMenuItem" id="separator6">
1194                                 <property name="visible">True</property>
1195                               </widget>
1196                             </child>
1197                           </widget>
1198                         </child>
1199                       </widget>
1200                     </child>
1201                     <child>
1202                       <widget class="GtkMenuItem" id="helpMenu">
1203                         <property name="visible">True</property>
1204                         <property name="label" translatable="yes">_Help</property>
1205                         <property name="use_underline">True</property>
1206                         <child>
1207                           <widget class="GtkMenu" id="helpMenu_menu">
1208                             <child>
1209                               <widget class="GtkImageMenuItem" id="contentsMenuItem">
1210                                 <property name="visible">True</property>
1211                                 <property name="label" translatable="yes">_Contents</property>
1212                                 <property name="use_underline">True</property>
1213                                 <accelerator key="F1" modifiers="" signal="activate"/>
1214                                 <child internal-child="image">
1215                                   <widget class="GtkImage" id="image1063">
1216                                     <property name="visible">True</property>
1217                                     <property name="stock">gtk-help</property>
1218                                     <property name="icon_size">1</property>
1219                                   </widget>
1220                                 </child>
1221                               </widget>
1222                             </child>
1223                             <child>
1224                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
1225                                 <property name="visible">True</property>
1226                                 <property name="label" translatable="yes">_About</property>
1227                                 <property name="use_underline">True</property>
1228                                 <child internal-child="image">
1229                                   <widget class="GtkImage" id="image1064">
1230                                     <property name="visible">True</property>
1231                                     <property name="stock">gtk-about</property>
1232                                     <property name="icon_size">1</property>
1233                                   </widget>
1234                                 </child>
1235                               </widget>
1236                             </child>
1237                           </widget>
1238                         </child>
1239                       </widget>
1240                     </child>
1241                   </widget>
1242                 </child>
1243               </widget>
1244               <packing>
1245                 <property name="expand">False</property>
1246                 <property name="fill">False</property>
1247               </packing>
1248             </child>
1249             <child>
1250               <widget class="GtkHBox" id="hbox9">
1251                 <property name="visible">True</property>
1252                 <child>
1253                   <widget class="GtkHPaned" id="hpaneScriptSequent">
1254                     <property name="visible">True</property>
1255                     <property name="can_focus">True</property>
1256                     <child>
1257                       <widget class="GtkHBox" id="hbox18">
1258                         <property name="visible">True</property>
1259                         <child>
1260                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1261                             <property name="visible">True</property>
1262                             <property name="shadow_type">GTK_SHADOW_OUT</property>
1263                             <property name="handle_position">GTK_POS_TOP</property>
1264                             <child>
1265                               <widget class="GtkTable" id="ToolBarTable">
1266                                 <property name="visible">True</property>
1267                                 <property name="n_rows">17</property>
1268                                 <property name="n_columns">2</property>
1269                                 <property name="row_spacing">4</property>
1270                                 <child>
1271                                   <placeholder/>
1272                                 </child>
1273                                 <child>
1274                                   <placeholder/>
1275                                 </child>
1276                                 <child>
1277                                   <placeholder/>
1278                                 </child>
1279                                 <child>
1280                                   <placeholder/>
1281                                 </child>
1282                                 <child>
1283                                   <placeholder/>
1284                                 </child>
1285                                 <child>
1286                                   <placeholder/>
1287                                 </child>
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                                   <widget class="GtkAlignment" id="alignment12">
1302                                     <property name="visible">True</property>
1303                                     <child>
1304                                       <placeholder/>
1305                                     </child>
1306                                   </widget>
1307                                   <packing>
1308                                     <property name="top_attach">15</property>
1309                                     <property name="bottom_attach">16</property>
1310                                     <property name="x_options">GTK_FILL</property>
1311                                   </packing>
1312                                 </child>
1313                                 <child>
1314                                   <widget class="GtkAlignment" id="alignment11">
1315                                     <property name="visible">True</property>
1316                                     <child>
1317                                       <placeholder/>
1318                                     </child>
1319                                   </widget>
1320                                   <packing>
1321                                     <property name="top_attach">13</property>
1322                                     <property name="bottom_attach">14</property>
1323                                     <property name="x_options">GTK_FILL</property>
1324                                   </packing>
1325                                 </child>
1326                                 <child>
1327                                   <widget class="GtkAlignment" id="alignment10">
1328                                     <property name="visible">True</property>
1329                                     <child>
1330                                       <placeholder/>
1331                                     </child>
1332                                   </widget>
1333                                   <packing>
1334                                     <property name="top_attach">10</property>
1335                                     <property name="bottom_attach">11</property>
1336                                     <property name="x_options">GTK_FILL</property>
1337                                   </packing>
1338                                 </child>
1339                                 <child>
1340                                   <widget class="GtkAlignment" id="alignment9">
1341                                     <property name="visible">True</property>
1342                                     <child>
1343                                       <placeholder/>
1344                                     </child>
1345                                   </widget>
1346                                   <packing>
1347                                     <property name="top_attach">7</property>
1348                                     <property name="bottom_attach">8</property>
1349                                     <property name="x_options">GTK_FILL</property>
1350                                   </packing>
1351                                 </child>
1352                                 <child>
1353                                   <widget class="GtkAlignment" id="alignment8">
1354                                     <property name="visible">True</property>
1355                                     <child>
1356                                       <placeholder/>
1357                                     </child>
1358                                   </widget>
1359                                   <packing>
1360                                     <property name="top_attach">5</property>
1361                                     <property name="bottom_attach">6</property>
1362                                     <property name="x_options">GTK_FILL</property>
1363                                   </packing>
1364                                 </child>
1365                                 <child>
1366                                   <widget class="GtkAlignment" id="alignment7">
1367                                     <property name="visible">True</property>
1368                                     <child>
1369                                       <placeholder/>
1370                                     </child>
1371                                   </widget>
1372                                   <packing>
1373                                     <property name="top_attach">3</property>
1374                                     <property name="bottom_attach">4</property>
1375                                     <property name="x_options">GTK_FILL</property>
1376                                   </packing>
1377                                 </child>
1378                                 <child>
1379                                   <widget class="GtkAlignment" id="alignment6">
1380                                     <property name="visible">True</property>
1381                                     <child>
1382                                       <placeholder/>
1383                                     </child>
1384                                   </widget>
1385                                   <packing>
1386                                     <property name="top_attach">1</property>
1387                                     <property name="bottom_attach">2</property>
1388                                     <property name="x_options">GTK_FILL</property>
1389                                   </packing>
1390                                 </child>
1391                                 <child>
1392                                   <widget class="GtkHBox" id="hbox17">
1393                                     <property name="visible">True</property>
1394                                     <property name="homogeneous">True</property>
1395                                     <child>
1396                                       <widget class="GtkButton" id="splitButton">
1397                                         <property name="visible">True</property>
1398                                         <property name="can_focus">True</property>
1399                                         <property name="tooltip" translatable="yes">Split</property>
1400                                         <property name="label" translatable="yes">∧</property>
1401                                         <property name="use_underline">True</property>
1402                                         <property name="response_id">0</property>
1403                                       </widget>
1404                                     </child>
1405                                     <child>
1406                                       <widget class="GtkButton" id="leftButton">
1407                                         <property name="visible">True</property>
1408                                         <property name="can_focus">True</property>
1409                                         <property name="tooltip" translatable="yes">Left</property>
1410                                         <property name="label" translatable="yes">L</property>
1411                                         <property name="use_underline">True</property>
1412                                         <property name="response_id">0</property>
1413                                       </widget>
1414                                       <packing>
1415                                         <property name="position">1</property>
1416                                       </packing>
1417                                     </child>
1418                                   </widget>
1419                                   <packing>
1420                                     <property name="top_attach">6</property>
1421                                     <property name="bottom_attach">7</property>
1422                                     <property name="x_options">GTK_FILL</property>
1423                                     <property name="y_options">GTK_FILL</property>
1424                                   </packing>
1425                                 </child>
1426                                 <child>
1427                                   <widget class="GtkHBox" id="hbox18">
1428                                     <property name="visible">True</property>
1429                                     <property name="homogeneous">True</property>
1430                                     <child>
1431                                       <widget class="GtkButton" id="rightButton">
1432                                         <property name="visible">True</property>
1433                                         <property name="can_focus">True</property>
1434                                         <property name="tooltip" translatable="yes">Right</property>
1435                                         <property name="label" translatable="yes">R</property>
1436                                         <property name="use_underline">True</property>
1437                                         <property name="response_id">0</property>
1438                                       </widget>
1439                                     </child>
1440                                     <child>
1441                                       <widget class="GtkButton" id="existsButton">
1442                                         <property name="visible">True</property>
1443                                         <property name="can_focus">True</property>
1444                                         <property name="tooltip" translatable="yes">Exists</property>
1445                                         <property name="label" translatable="yes">∃</property>
1446                                         <property name="use_underline">True</property>
1447                                         <property name="response_id">0</property>
1448                                       </widget>
1449                                       <packing>
1450                                         <property name="position">1</property>
1451                                       </packing>
1452                                     </child>
1453                                   </widget>
1454                                   <packing>
1455                                     <property name="left_attach">1</property>
1456                                     <property name="right_attach">2</property>
1457                                     <property name="top_attach">6</property>
1458                                     <property name="bottom_attach">7</property>
1459                                     <property name="x_options">GTK_FILL</property>
1460                                     <property name="y_options">GTK_FILL</property>
1461                                   </packing>
1462                                 </child>
1463                                 <child>
1464                                   <widget class="GtkButton" id="elimTypeButton">
1465                                     <property name="visible">True</property>
1466                                     <property name="can_focus">True</property>
1467                                     <property name="tooltip" translatable="yes">ElimType</property>
1468                                     <property name="label" translatable="yes">elimTy</property>
1469                                     <property name="use_underline">True</property>
1470                                     <property name="response_id">0</property>
1471                                   </widget>
1472                                   <packing>
1473                                     <property name="left_attach">1</property>
1474                                     <property name="right_attach">2</property>
1475                                     <property name="top_attach">4</property>
1476                                     <property name="bottom_attach">5</property>
1477                                     <property name="x_options">GTK_FILL</property>
1478                                     <property name="y_options"></property>
1479                                   </packing>
1480                                 </child>
1481                                 <child>
1482                                   <widget class="GtkButton" id="replaceButton">
1483                                     <property name="visible">True</property>
1484                                     <property name="can_focus">True</property>
1485                                     <property name="tooltip" translatable="yes">Replace</property>
1486                                     <property name="label" translatable="yes">repl</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">16</property>
1494                                     <property name="bottom_attach">17</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="cutButton">
1501                                     <property name="visible">True</property>
1502                                     <property name="can_focus">True</property>
1503                                     <property name="tooltip" translatable="yes">Cut</property>
1504                                     <property name="label" translatable="yes">cut</property>
1505                                     <property name="use_underline">True</property>
1506                                     <property name="response_id">0</property>
1507                                   </widget>
1508                                   <packing>
1509                                     <property name="top_attach">16</property>
1510                                     <property name="bottom_attach">17</property>
1511                                     <property name="x_options">GTK_FILL</property>
1512                                     <property name="y_options"></property>
1513                                   </packing>
1514                                 </child>
1515                                 <child>
1516                                   <widget class="GtkButton" id="autoButton">
1517                                     <property name="visible">True</property>
1518                                     <property name="can_focus">True</property>
1519                                     <property name="tooltip" translatable="yes">Auto</property>
1520                                     <property name="label" translatable="yes">auto</property>
1521                                     <property name="use_underline">True</property>
1522                                     <property name="response_id">0</property>
1523                                   </widget>
1524                                   <packing>
1525                                     <property name="left_attach">1</property>
1526                                     <property name="right_attach">2</property>
1527                                     <property name="top_attach">14</property>
1528                                     <property name="bottom_attach">15</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="assumptionButton">
1535                                     <property name="visible">True</property>
1536                                     <property name="can_focus">True</property>
1537                                     <property name="tooltip" translatable="yes">Assumption</property>
1538                                     <property name="label" translatable="yes">assum</property>
1539                                     <property name="use_underline">True</property>
1540                                     <property name="response_id">0</property>
1541                                   </widget>
1542                                   <packing>
1543                                     <property name="top_attach">14</property>
1544                                     <property name="bottom_attach">15</property>
1545                                     <property name="x_options">GTK_FILL</property>
1546                                     <property name="y_options"></property>
1547                                   </packing>
1548                                 </child>
1549                                 <child>
1550                                   <widget class="GtkButton" id="whdButton">
1551                                     <property name="visible">True</property>
1552                                     <property name="can_focus">True</property>
1553                                     <property name="tooltip" translatable="yes">Whd</property>
1554                                     <property name="label" translatable="yes">whd</property>
1555                                     <property name="use_underline">True</property>
1556                                     <property name="response_id">0</property>
1557                                   </widget>
1558                                   <packing>
1559                                     <property name="top_attach">12</property>
1560                                     <property name="bottom_attach">13</property>
1561                                     <property name="x_options">GTK_FILL</property>
1562                                     <property name="y_options"></property>
1563                                   </packing>
1564                                 </child>
1565                                 <child>
1566                                   <widget class="GtkButton" id="reduceButton">
1567                                     <property name="visible">True</property>
1568                                     <property name="can_focus">True</property>
1569                                     <property name="tooltip" translatable="yes">Reduce</property>
1570                                     <property name="label" translatable="yes">red</property>
1571                                     <property name="use_underline">True</property>
1572                                     <property name="response_id">0</property>
1573                                   </widget>
1574                                   <packing>
1575                                     <property name="left_attach">1</property>
1576                                     <property name="right_attach">2</property>
1577                                     <property name="top_attach">11</property>
1578                                     <property name="bottom_attach">12</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="simplifyButton">
1585                                     <property name="visible">True</property>
1586                                     <property name="can_focus">True</property>
1587                                     <property name="tooltip" translatable="yes">Simplify</property>
1588                                     <property name="label" translatable="yes">simpl</property>
1589                                     <property name="use_underline">True</property>
1590                                     <property name="response_id">0</property>
1591                                   </widget>
1592                                   <packing>
1593                                     <property name="top_attach">11</property>
1594                                     <property name="bottom_attach">12</property>
1595                                     <property name="x_options">GTK_FILL</property>
1596                                     <property name="y_options"></property>
1597                                   </packing>
1598                                 </child>
1599                                 <child>
1600                                   <widget class="GtkButton" id="transitivityButton">
1601                                     <property name="visible">True</property>
1602                                     <property name="can_focus">True</property>
1603                                     <property name="tooltip" translatable="yes">Transitivity</property>
1604                                     <property name="label" translatable="yes">trans</property>
1605                                     <property name="use_underline">True</property>
1606                                     <property name="response_id">0</property>
1607                                   </widget>
1608                                   <packing>
1609                                     <property name="top_attach">9</property>
1610                                     <property name="bottom_attach">10</property>
1611                                     <property name="x_options">GTK_FILL</property>
1612                                     <property name="y_options"></property>
1613                                   </packing>
1614                                 </child>
1615                                 <child>
1616                                   <widget class="GtkButton" id="symmetryButton">
1617                                     <property name="visible">True</property>
1618                                     <property name="can_focus">True</property>
1619                                     <property name="tooltip" translatable="yes">Symmetry</property>
1620                                     <property name="label" translatable="yes">sym</property>
1621                                     <property name="use_underline">True</property>
1622                                     <property name="response_id">0</property>
1623                                   </widget>
1624                                   <packing>
1625                                     <property name="left_attach">1</property>
1626                                     <property name="right_attach">2</property>
1627                                     <property name="top_attach">8</property>
1628                                     <property name="bottom_attach">9</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="reflexivityButton">
1635                                     <property name="visible">True</property>
1636                                     <property name="can_focus">True</property>
1637                                     <property name="tooltip" translatable="yes">Reflexivity</property>
1638                                     <property name="label" translatable="yes">refl</property>
1639                                     <property name="use_underline">True</property>
1640                                     <property name="response_id">0</property>
1641                                   </widget>
1642                                   <packing>
1643                                     <property name="top_attach">8</property>
1644                                     <property name="bottom_attach">9</property>
1645                                     <property name="x_options">GTK_FILL</property>
1646                                     <property name="y_options"></property>
1647                                   </packing>
1648                                 </child>
1649                                 <child>
1650                                   <widget class="GtkButton" id="elimButton">
1651                                     <property name="visible">True</property>
1652                                     <property name="can_focus">True</property>
1653                                     <property name="tooltip" translatable="yes">Elim</property>
1654                                     <property name="label" translatable="yes">elim</property>
1655                                     <property name="use_underline">True</property>
1656                                     <property name="response_id">0</property>
1657                                   </widget>
1658                                   <packing>
1659                                     <property name="top_attach">4</property>
1660                                     <property name="bottom_attach">5</property>
1661                                     <property name="x_options">GTK_FILL</property>
1662                                     <property name="y_options"></property>
1663                                   </packing>
1664                                 </child>
1665                                 <child>
1666                                   <widget class="GtkButton" id="exactButton">
1667                                     <property name="visible">True</property>
1668                                     <property name="can_focus">True</property>
1669                                     <property name="tooltip" translatable="yes">Exact</property>
1670                                     <property name="label" translatable="yes">exact</property>
1671                                     <property name="use_underline">True</property>
1672                                     <property name="response_id">0</property>
1673                                   </widget>
1674                                   <packing>
1675                                     <property name="top_attach">2</property>
1676                                     <property name="bottom_attach">3</property>
1677                                     <property name="x_options">GTK_FILL</property>
1678                                     <property name="y_options"></property>
1679                                   </packing>
1680                                 </child>
1681                                 <child>
1682                                   <widget class="GtkButton" id="introsButton">
1683                                     <property name="visible">True</property>
1684                                     <property name="can_focus">True</property>
1685                                     <property name="tooltip" translatable="yes">Intros</property>
1686                                     <property name="label" translatable="yes">intro</property>
1687                                     <property name="use_underline">True</property>
1688                                     <property name="response_id">0</property>
1689                                   </widget>
1690                                   <packing>
1691                                     <property name="x_options">GTK_FILL</property>
1692                                     <property name="y_options"></property>
1693                                   </packing>
1694                                 </child>
1695                                 <child>
1696                                   <widget class="GtkButton" id="applyButton">
1697                                     <property name="visible">True</property>
1698                                     <property name="can_focus">True</property>
1699                                     <property name="tooltip" translatable="yes">Apply</property>
1700                                     <property name="label" translatable="yes">apply</property>
1701                                     <property name="use_underline">True</property>
1702                                     <property name="response_id">0</property>
1703                                   </widget>
1704                                   <packing>
1705                                     <property name="left_attach">1</property>
1706                                     <property name="right_attach">2</property>
1707                                     <property name="x_options">GTK_FILL</property>
1708                                     <property name="y_options"></property>
1709                                   </packing>
1710                                 </child>
1711                               </widget>
1712                             </child>
1713                           </widget>
1714                           <packing>
1715                             <property name="expand">False</property>
1716                           </packing>
1717                         </child>
1718                         <child>
1719                           <widget class="GtkVBox" id="vboxScript">
1720                             <property name="width_request">400</property>
1721                             <property name="visible">True</property>
1722                             <child>
1723                               <widget class="GtkHBox" id="hbox28">
1724                                 <property name="visible">True</property>
1725                                 <child>
1726                                   <widget class="GtkToolbar" id="buttonsToolbar">
1727                                     <property name="visible">True</property>
1728                                     <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1729                                     <child>
1730                                       <widget class="GtkToolItem" id="toolitem41">
1731                                         <property name="visible">True</property>
1732                                         <child>
1733                                           <widget class="GtkButton" id="scriptTopButton">
1734                                             <property name="visible">True</property>
1735                                             <property name="can_focus">True</property>
1736                                             <property name="tooltip" translatable="yes">Restart</property>
1737                                             <property name="relief">GTK_RELIEF_NONE</property>
1738                                             <property name="response_id">0</property>
1739                                             <child>
1740                                               <widget class="GtkImage" id="image920">
1741                                                 <property name="visible">True</property>
1742                                                 <property name="stock">gtk-goto-top</property>
1743                                               </widget>
1744                                             </child>
1745                                           </widget>
1746                                         </child>
1747                                       </widget>
1748                                       <packing>
1749                                         <property name="expand">False</property>
1750                                         <property name="homogeneous">False</property>
1751                                       </packing>
1752                                     </child>
1753                                     <child>
1754                                       <widget class="GtkToolItem" id="toolitem42">
1755                                         <property name="visible">True</property>
1756                                         <child>
1757                                           <widget class="GtkButton" id="scriptRetractButton">
1758                                             <property name="visible">True</property>
1759                                             <property name="can_focus">True</property>
1760                                             <property name="tooltip" translatable="yes">Retract 1 phrase</property>
1761                                             <property name="relief">GTK_RELIEF_NONE</property>
1762                                             <property name="response_id">0</property>
1763                                             <child>
1764                                               <widget class="GtkImage" id="image921">
1765                                                 <property name="visible">True</property>
1766                                                 <property name="stock">gtk-go-up</property>
1767                                               </widget>
1768                                             </child>
1769                                           </widget>
1770                                         </child>
1771                                       </widget>
1772                                       <packing>
1773                                         <property name="expand">False</property>
1774                                         <property name="homogeneous">False</property>
1775                                       </packing>
1776                                     </child>
1777                                     <child>
1778                                       <widget class="GtkToolItem" id="toolitem43">
1779                                         <property name="visible">True</property>
1780                                         <child>
1781                                           <widget class="GtkButton" id="scriptJumpButton">
1782                                             <property name="visible">True</property>
1783                                             <property name="can_focus">True</property>
1784                                             <property name="tooltip" translatable="yes">Execute until point</property>
1785                                             <property name="relief">GTK_RELIEF_NONE</property>
1786                                             <property name="response_id">0</property>
1787                                             <child>
1788                                               <widget class="GtkImage" id="image922">
1789                                                 <property name="visible">True</property>
1790                                                 <property name="stock">gtk-jump-to</property>
1791                                               </widget>
1792                                             </child>
1793                                           </widget>
1794                                         </child>
1795                                       </widget>
1796                                       <packing>
1797                                         <property name="expand">False</property>
1798                                         <property name="homogeneous">False</property>
1799                                       </packing>
1800                                     </child>
1801                                     <child>
1802                                       <widget class="GtkToolItem" id="toolitem44">
1803                                         <property name="visible">True</property>
1804                                         <child>
1805                                           <widget class="GtkButton" id="scriptAdvanceButton">
1806                                             <property name="visible">True</property>
1807                                             <property name="can_focus">True</property>
1808                                             <property name="tooltip" translatable="yes">Execute 1 phrase</property>
1809                                             <property name="relief">GTK_RELIEF_NONE</property>
1810                                             <property name="response_id">0</property>
1811                                             <child>
1812                                               <widget class="GtkImage" id="image923">
1813                                                 <property name="visible">True</property>
1814                                                 <property name="stock">gtk-go-down</property>
1815                                               </widget>
1816                                             </child>
1817                                           </widget>
1818                                         </child>
1819                                       </widget>
1820                                       <packing>
1821                                         <property name="expand">False</property>
1822                                         <property name="homogeneous">False</property>
1823                                       </packing>
1824                                     </child>
1825                                     <child>
1826                                       <widget class="GtkToolItem" id="toolitem45">
1827                                         <property name="visible">True</property>
1828                                         <child>
1829                                           <widget class="GtkButton" id="scriptBottomButton">
1830                                             <property name="visible">True</property>
1831                                             <property name="can_focus">True</property>
1832                                             <property name="tooltip" translatable="yes">Execute all</property>
1833                                             <property name="relief">GTK_RELIEF_NONE</property>
1834                                             <property name="response_id">0</property>
1835                                             <child>
1836                                               <widget class="GtkImage" id="image924">
1837                                                 <property name="visible">True</property>
1838                                                 <property name="stock">gtk-goto-bottom</property>
1839                                               </widget>
1840                                             </child>
1841                                           </widget>
1842                                         </child>
1843                                       </widget>
1844                                       <packing>
1845                                         <property name="expand">False</property>
1846                                         <property name="homogeneous">False</property>
1847                                       </packing>
1848                                     </child>
1849                                   </widget>
1850                                 </child>
1851                                 <child>
1852                                   <widget class="GtkToolbar" id="toolbar2">
1853                                     <property name="visible">True</property>
1854                                     <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
1855                                     <child>
1856                                       <widget class="GtkToolItem" id="toolitem46">
1857                                         <property name="visible">True</property>
1858                                         <child>
1859                                           <widget class="GtkButton" id="scriptAbortButton">
1860                                             <property name="visible">True</property>
1861                                             <property name="can_focus">True</property>
1862                                             <property name="relief">GTK_RELIEF_NONE</property>
1863                                             <property name="response_id">0</property>
1864                                             <child>
1865                                               <widget class="GtkImage" id="image927">
1866                                                 <property name="visible">True</property>
1867                                                 <property name="stock">gtk-stop</property>
1868                                               </widget>
1869                                             </child>
1870                                           </widget>
1871                                         </child>
1872                                       </widget>
1873                                       <packing>
1874                                         <property name="expand">False</property>
1875                                         <property name="homogeneous">False</property>
1876                                       </packing>
1877                                     </child>
1878                                   </widget>
1879                                   <packing>
1880                                     <property name="expand">False</property>
1881                                     <property name="position">1</property>
1882                                   </packing>
1883                                 </child>
1884                               </widget>
1885                               <packing>
1886                                 <property name="expand">False</property>
1887                                 <property name="fill">False</property>
1888                               </packing>
1889                             </child>
1890                             <child>
1891                               <widget class="GtkNotebook" id="scriptNotebook">
1892                                 <property name="visible">True</property>
1893                                 <property name="can_focus">True</property>
1894                                 <property name="tab_pos">GTK_POS_BOTTOM</property>
1895                                 <child>
1896                                   <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
1897                                     <property name="visible">True</property>
1898                                     <property name="can_focus">True</property>
1899                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1900                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1901                                     <child>
1902                                       <placeholder/>
1903                                     </child>
1904                                   </widget>
1905                                   <packing>
1906                                     <property name="tab_expand">False</property>
1907                                   </packing>
1908                                 </child>
1909                                 <child>
1910                                   <widget class="GtkLabel" id="scriptLabel">
1911                                     <property name="visible">True</property>
1912                                     <property name="label" translatable="yes">script</property>
1913                                   </widget>
1914                                   <packing>
1915                                     <property name="type">tab</property>
1916                                     <property name="tab_expand">False</property>
1917                                     <property name="tab_fill">False</property>
1918                                   </packing>
1919                                 </child>
1920                                 <child>
1921                                   <widget class="GtkScrolledWindow" id="scrolledwindow8">
1922                                     <property name="visible">True</property>
1923                                     <property name="can_focus">True</property>
1924                                     <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1925                                     <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1926                                     <child>
1927                                       <widget class="GtkViewport" id="viewport1">
1928                                         <property name="visible">True</property>
1929                                         <child>
1930                                           <widget class="GtkLabel" id="label25">
1931                                             <property name="visible">True</property>
1932                                             <property name="label" translatable="yes">Not implemented.</property>
1933                                           </widget>
1934                                         </child>
1935                                       </widget>
1936                                     </child>
1937                                   </widget>
1938                                   <packing>
1939                                     <property name="position">1</property>
1940                                     <property name="tab_expand">False</property>
1941                                   </packing>
1942                                 </child>
1943                                 <child>
1944                                   <widget class="GtkLabel" id="label13">
1945                                     <property name="visible">True</property>
1946                                     <property name="label" translatable="yes">outline</property>
1947                                   </widget>
1948                                   <packing>
1949                                     <property name="type">tab</property>
1950                                     <property name="position">1</property>
1951                                     <property name="tab_expand">False</property>
1952                                     <property name="tab_fill">False</property>
1953                                   </packing>
1954                                 </child>
1955                               </widget>
1956                               <packing>
1957                                 <property name="position">1</property>
1958                               </packing>
1959                             </child>
1960                           </widget>
1961                           <packing>
1962                             <property name="position">1</property>
1963                           </packing>
1964                         </child>
1965                       </widget>
1966                       <packing>
1967                         <property name="resize">False</property>
1968                         <property name="shrink">True</property>
1969                       </packing>
1970                     </child>
1971                     <child>
1972                       <widget class="GtkVPaned" id="vpaned1">
1973                         <property name="width_request">250</property>
1974                         <property name="height_request">500</property>
1975                         <property name="visible">True</property>
1976                         <property name="can_focus">True</property>
1977                         <property name="position">380</property>
1978                         <child>
1979                           <widget class="GtkNotebook" id="sequentsNotebook">
1980                             <property name="visible">True</property>
1981                             <property name="can_focus">True</property>
1982                           </widget>
1983                           <packing>
1984                             <property name="resize">False</property>
1985                             <property name="shrink">True</property>
1986                           </packing>
1987                         </child>
1988                         <child>
1989                           <widget class="GtkHBox" id="hbox9">
1990                             <property name="visible">True</property>
1991                             <child>
1992                               <widget class="GtkScrolledWindow" id="logScrolledWin">
1993                                 <property name="visible">True</property>
1994                                 <property name="can_focus">True</property>
1995                                 <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
1996                                 <property name="shadow_type">GTK_SHADOW_IN</property>
1997                                 <child>
1998                                   <widget class="GtkTextView" id="logTextView">
1999                                     <property name="visible">True</property>
2000                                     <property name="can_focus">True</property>
2001                                     <property name="editable">False</property>
2002                                     <property name="wrap_mode">GTK_WRAP_CHAR</property>
2003                                     <property name="cursor_visible">False</property>
2004                                   </widget>
2005                                 </child>
2006                               </widget>
2007                             </child>
2008                           </widget>
2009                           <packing>
2010                             <property name="resize">True</property>
2011                             <property name="shrink">True</property>
2012                           </packing>
2013                         </child>
2014                       </widget>
2015                       <packing>
2016                         <property name="resize">True</property>
2017                         <property name="shrink">True</property>
2018                       </packing>
2019                     </child>
2020                   </widget>
2021                 </child>
2022               </widget>
2023               <packing>
2024                 <property name="position">1</property>
2025               </packing>
2026             </child>
2027             <child>
2028               <widget class="GtkHBox" id="hbox10">
2029                 <property name="visible">True</property>
2030                 <child>
2031                   <widget class="GtkStatusbar" id="StatusBar">
2032                     <property name="visible">True</property>
2033                     <property name="has_resize_grip">False</property>
2034                   </widget>
2035                 </child>
2036                 <child>
2037                   <widget class="GtkNotebook" id="HintNotebook">
2038                     <property name="visible">True</property>
2039                     <property name="show_tabs">False</property>
2040                     <child>
2041                       <widget class="GtkImage" id="HintLowImage">
2042                         <property name="visible">True</property>
2043                         <property name="stock">gtk-missing-image</property>
2044                       </widget>
2045                       <packing>
2046                         <property name="tab_expand">False</property>
2047                       </packing>
2048                     </child>
2049                     <child>
2050                       <widget class="GtkLabel" id="label14">
2051                         <property name="visible">True</property>
2052                         <property name="label" translatable="yes">label14</property>
2053                       </widget>
2054                       <packing>
2055                         <property name="type">tab</property>
2056                         <property name="tab_expand">False</property>
2057                         <property name="tab_fill">False</property>
2058                       </packing>
2059                     </child>
2060                     <child>
2061                       <widget class="GtkImage" id="HintMediumImage">
2062                         <property name="visible">True</property>
2063                         <property name="stock">gtk-missing-image</property>
2064                       </widget>
2065                       <packing>
2066                         <property name="position">1</property>
2067                         <property name="tab_expand">False</property>
2068                       </packing>
2069                     </child>
2070                     <child>
2071                       <widget class="GtkLabel" id="label15">
2072                         <property name="visible">True</property>
2073                         <property name="label" translatable="yes">label15</property>
2074                       </widget>
2075                       <packing>
2076                         <property name="type">tab</property>
2077                         <property name="position">1</property>
2078                         <property name="tab_expand">False</property>
2079                         <property name="tab_fill">False</property>
2080                       </packing>
2081                     </child>
2082                     <child>
2083                       <widget class="GtkImage" id="HintHighImage">
2084                         <property name="visible">True</property>
2085                         <property name="stock">gtk-missing-image</property>
2086                       </widget>
2087                       <packing>
2088                         <property name="position">2</property>
2089                         <property name="tab_expand">False</property>
2090                       </packing>
2091                     </child>
2092                     <child>
2093                       <widget class="GtkLabel" id="label16">
2094                         <property name="visible">True</property>
2095                         <property name="label" translatable="yes">label16</property>
2096                       </widget>
2097                       <packing>
2098                         <property name="type">tab</property>
2099                         <property name="position">2</property>
2100                         <property name="tab_expand">False</property>
2101                         <property name="tab_fill">False</property>
2102                       </packing>
2103                     </child>
2104                   </widget>
2105                   <packing>
2106                     <property name="expand">False</property>
2107                     <property name="position">1</property>
2108                   </packing>
2109                 </child>
2110               </widget>
2111               <packing>
2112                 <property name="expand">False</property>
2113                 <property name="fill">False</property>
2114                 <property name="position">2</property>
2115               </packing>
2116             </child>
2117           </widget>
2118         </child>
2119       </widget>
2120     </child>
2121   </widget>
2122   <widget class="GtkDialog" id="TextDialog">
2123     <property name="title" translatable="yes">DUMMY</property>
2124     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2125     <child internal-child="vbox">
2126       <widget class="GtkVBox" id="vbox5">
2127         <property name="visible">True</property>
2128         <child>
2129           <widget class="GtkLabel" id="TextDialogLabel">
2130             <property name="visible">True</property>
2131             <property name="label" translatable="yes">DUMMY</property>
2132           </widget>
2133           <packing>
2134             <property name="expand">False</property>
2135             <property name="fill">False</property>
2136             <property name="position">2</property>
2137           </packing>
2138         </child>
2139         <child>
2140           <widget class="GtkScrolledWindow" id="scrolledwindow2">
2141             <property name="visible">True</property>
2142             <property name="can_focus">True</property>
2143             <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2144             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2145             <property name="shadow_type">GTK_SHADOW_IN</property>
2146             <child>
2147               <widget class="GtkTextView" id="TextDialogTextView">
2148                 <property name="visible">True</property>
2149                 <property name="can_focus">True</property>
2150               </widget>
2151             </child>
2152           </widget>
2153           <packing>
2154             <property name="position">3</property>
2155           </packing>
2156         </child>
2157         <child internal-child="action_area">
2158           <widget class="GtkHButtonBox" id="hbuttonbox1">
2159             <property name="visible">True</property>
2160             <property name="layout_style">GTK_BUTTONBOX_END</property>
2161             <child>
2162               <widget class="GtkButton" id="TextDialogCancelButton">
2163                 <property name="visible">True</property>
2164                 <property name="can_focus">True</property>
2165                 <property name="can_default">True</property>
2166                 <property name="label">gtk-cancel</property>
2167                 <property name="use_stock">True</property>
2168                 <property name="response_id">-6</property>
2169               </widget>
2170             </child>
2171             <child>
2172               <widget class="GtkButton" id="TextDialogOkButton">
2173                 <property name="visible">True</property>
2174                 <property name="can_focus">True</property>
2175                 <property name="can_default">True</property>
2176                 <property name="label">gtk-ok</property>
2177                 <property name="use_stock">True</property>
2178                 <property name="response_id">-5</property>
2179               </widget>
2180               <packing>
2181                 <property name="position">1</property>
2182               </packing>
2183             </child>
2184           </widget>
2185           <packing>
2186             <property name="expand">False</property>
2187             <property name="pack_type">GTK_PACK_END</property>
2188           </packing>
2189         </child>
2190       </widget>
2191     </child>
2192   </widget>
2193   <widget class="GtkDialog" id="UriChoiceDialog">
2194     <property name="height_request">280</property>
2195     <property name="title" translatable="yes">Uri choice</property>
2196     <property name="modal">True</property>
2197     <property name="window_position">GTK_WIN_POS_CENTER</property>
2198     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2199     <child internal-child="vbox">
2200       <widget class="GtkVBox" id="dialog-vbox3">
2201         <property name="visible">True</property>
2202         <property name="spacing">4</property>
2203         <child>
2204           <widget class="GtkVBox" id="vbox2">
2205             <property name="visible">True</property>
2206             <property name="spacing">3</property>
2207             <child>
2208               <widget class="GtkLabel" id="UriChoiceLabel">
2209                 <property name="visible">True</property>
2210                 <property name="label" translatable="yes">some informative message here ...</property>
2211               </widget>
2212               <packing>
2213                 <property name="expand">False</property>
2214                 <property name="fill">False</property>
2215               </packing>
2216             </child>
2217             <child>
2218               <widget class="GtkScrolledWindow" id="scrolledwindow1">
2219                 <property name="width_request">400</property>
2220                 <property name="visible">True</property>
2221                 <property name="can_focus">True</property>
2222                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2223                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2224                 <child>
2225                   <widget class="GtkTreeView" id="UriChoiceTreeView">
2226                     <property name="visible">True</property>
2227                     <property name="can_focus">True</property>
2228                     <property name="headers_visible">False</property>
2229                   </widget>
2230                 </child>
2231               </widget>
2232               <packing>
2233                 <property name="position">1</property>
2234               </packing>
2235             </child>
2236             <child>
2237               <widget class="GtkHBox" id="uriEntryHBox">
2238                 <property name="visible">True</property>
2239                 <child>
2240                   <widget class="GtkLabel" id="label2">
2241                     <property name="visible">True</property>
2242                     <property name="label" translatable="yes">URI: </property>
2243                   </widget>
2244                   <packing>
2245                     <property name="expand">False</property>
2246                     <property name="fill">False</property>
2247                   </packing>
2248                 </child>
2249                 <child>
2250                   <widget class="GtkEntry" id="entry1">
2251                     <property name="visible">True</property>
2252                     <property name="can_focus">True</property>
2253                     <property name="invisible_char">*</property>
2254                   </widget>
2255                   <packing>
2256                     <property name="position">1</property>
2257                   </packing>
2258                 </child>
2259               </widget>
2260               <packing>
2261                 <property name="expand">False</property>
2262                 <property name="position">2</property>
2263               </packing>
2264             </child>
2265           </widget>
2266           <packing>
2267             <property name="position">2</property>
2268           </packing>
2269         </child>
2270         <child internal-child="action_area">
2271           <widget class="GtkHButtonBox" id="dialog-action_area3">
2272             <property name="visible">True</property>
2273             <property name="layout_style">GTK_BUTTONBOX_END</property>
2274             <child>
2275               <widget class="GtkButton" id="UriChoiceAbortButton">
2276                 <property name="visible">True</property>
2277                 <property name="can_focus">True</property>
2278                 <property name="can_default">True</property>
2279                 <property name="label">gtk-cancel</property>
2280                 <property name="use_stock">True</property>
2281                 <property name="response_id">-6</property>
2282               </widget>
2283             </child>
2284             <child>
2285               <widget class="GtkButton" id="UriChoiceSelectedButton">
2286                 <property name="visible">True</property>
2287                 <property name="can_focus">True</property>
2288                 <property name="can_default">True</property>
2289                 <property name="response_id">0</property>
2290                 <child>
2291                   <widget class="GtkAlignment" id="alignment2">
2292                     <property name="visible">True</property>
2293                     <property name="xscale">0</property>
2294                     <property name="yscale">0</property>
2295                     <child>
2296                       <widget class="GtkHBox" id="hbox3">
2297                         <property name="visible">True</property>
2298                         <property name="spacing">2</property>
2299                         <child>
2300                           <widget class="GtkImage" id="image19">
2301                             <property name="visible">True</property>
2302                             <property name="stock">gtk-index</property>
2303                           </widget>
2304                           <packing>
2305                             <property name="expand">False</property>
2306                             <property name="fill">False</property>
2307                           </packing>
2308                         </child>
2309                         <child>
2310                           <widget class="GtkLabel" id="label3">
2311                             <property name="visible">True</property>
2312                             <property name="label" translatable="yes">Try _Selected</property>
2313                             <property name="use_underline">True</property>
2314                           </widget>
2315                           <packing>
2316                             <property name="expand">False</property>
2317                             <property name="fill">False</property>
2318                             <property name="position">1</property>
2319                           </packing>
2320                         </child>
2321                       </widget>
2322                     </child>
2323                   </widget>
2324                 </child>
2325               </widget>
2326               <packing>
2327                 <property name="position">1</property>
2328               </packing>
2329             </child>
2330             <child>
2331               <widget class="GtkButton" id="UriChoiceConstantsButton">
2332                 <property name="visible">True</property>
2333                 <property name="sensitive">False</property>
2334                 <property name="can_focus">True</property>
2335                 <property name="can_default">True</property>
2336                 <property name="label" translatable="yes">Try Constants</property>
2337                 <property name="use_underline">True</property>
2338                 <property name="response_id">0</property>
2339               </widget>
2340               <packing>
2341                 <property name="position">2</property>
2342               </packing>
2343             </child>
2344             <child>
2345               <widget class="GtkButton" id="copyButton">
2346                 <property name="can_focus">True</property>
2347                 <property name="can_default">True</property>
2348                 <property name="label">gtk-copy</property>
2349                 <property name="use_stock">True</property>
2350                 <property name="response_id">0</property>
2351               </widget>
2352               <packing>
2353                 <property name="position">3</property>
2354               </packing>
2355             </child>
2356             <child>
2357               <widget class="GtkButton" id="uriChoiceAutoButton">
2358                 <property name="visible">True</property>
2359                 <property name="can_focus">True</property>
2360                 <property name="can_default">True</property>
2361                 <property name="response_id">0</property>
2362                 <child>
2363                   <widget class="GtkAlignment" id="alignment5">
2364                     <property name="visible">True</property>
2365                     <property name="xscale">0</property>
2366                     <property name="yscale">0</property>
2367                     <child>
2368                       <widget class="GtkHBox" id="hbox16">
2369                         <property name="visible">True</property>
2370                         <property name="spacing">2</property>
2371                         <child>
2372                           <widget class="GtkImage" id="image302">
2373                             <property name="visible">True</property>
2374                             <property name="stock">gtk-ok</property>
2375                           </widget>
2376                           <packing>
2377                             <property name="expand">False</property>
2378                             <property name="fill">False</property>
2379                           </packing>
2380                         </child>
2381                         <child>
2382                           <widget class="GtkLabel" id="okLabel">
2383                             <property name="visible">True</property>
2384                             <property name="label" translatable="yes">bla bla bla</property>
2385                             <property name="use_underline">True</property>
2386                           </widget>
2387                           <packing>
2388                             <property name="expand">False</property>
2389                             <property name="fill">False</property>
2390                             <property name="position">1</property>
2391                           </packing>
2392                         </child>
2393                       </widget>
2394                     </child>
2395                   </widget>
2396                 </child>
2397               </widget>
2398               <packing>
2399                 <property name="position">4</property>
2400               </packing>
2401             </child>
2402             <child>
2403               <widget class="GtkButton" id="uriChoiceForwardButton">
2404                 <property name="visible">True</property>
2405                 <property name="can_focus">True</property>
2406                 <property name="can_default">True</property>
2407                 <property name="label">gtk-go-forward</property>
2408                 <property name="use_stock">True</property>
2409                 <property name="response_id">0</property>
2410               </widget>
2411               <packing>
2412                 <property name="position">5</property>
2413               </packing>
2414             </child>
2415           </widget>
2416           <packing>
2417             <property name="expand">False</property>
2418             <property name="pack_type">GTK_PACK_END</property>
2419           </packing>
2420         </child>
2421       </widget>
2422     </child>
2423   </widget>
2424   <widget class="GtkWindow" id="FindReplWin">
2425     <property name="border_width">5</property>
2426     <property name="title" translatable="yes">Find &amp; Replace</property>
2427     <property name="resizable">False</property>
2428     <property name="window_position">GTK_WIN_POS_MOUSE</property>
2429     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2430     <child>
2431       <widget class="GtkTable" id="table1">
2432         <property name="visible">True</property>
2433         <property name="n_rows">3</property>
2434         <property name="n_columns">2</property>
2435         <property name="row_spacing">5</property>
2436         <child>
2437           <widget class="GtkHBox" id="hbox19">
2438             <property name="visible">True</property>
2439             <property name="spacing">5</property>
2440             <child>
2441               <widget class="GtkVBox" id="vbox9">
2442                 <property name="visible">True</property>
2443                 <child>
2444                   <placeholder/>
2445                 </child>
2446                 <child>
2447                   <placeholder/>
2448                 </child>
2449               </widget>
2450             </child>
2451             <child>
2452               <widget class="GtkButton" id="findButton">
2453                 <property name="visible">True</property>
2454                 <property name="can_focus">True</property>
2455                 <property name="label">gtk-find</property>
2456                 <property name="use_stock">True</property>
2457                 <property name="response_id">0</property>
2458               </widget>
2459               <packing>
2460                 <property name="expand">False</property>
2461                 <property name="fill">False</property>
2462                 <property name="position">1</property>
2463               </packing>
2464             </child>
2465             <child>
2466               <widget class="GtkButton" id="findReplButton">
2467                 <property name="visible">True</property>
2468                 <property name="can_focus">True</property>
2469                 <property name="response_id">0</property>
2470                 <child>
2471                   <widget class="GtkAlignment" id="alignment13">
2472                     <property name="visible">True</property>
2473                     <property name="xscale">0</property>
2474                     <property name="yscale">0</property>
2475                     <child>
2476                       <widget class="GtkHBox" id="hbox20">
2477                         <property name="visible">True</property>
2478                         <property name="spacing">2</property>
2479                         <child>
2480                           <widget class="GtkImage" id="image357">
2481                             <property name="visible">True</property>
2482                             <property name="stock">gtk-find-and-replace</property>
2483                           </widget>
2484                           <packing>
2485                             <property name="expand">False</property>
2486                             <property name="fill">False</property>
2487                           </packing>
2488                         </child>
2489                         <child>
2490                           <widget class="GtkLabel" id="label19">
2491                             <property name="visible">True</property>
2492                             <property name="label">_Replace</property>
2493                             <property name="use_underline">True</property>
2494                           </widget>
2495                           <packing>
2496                             <property name="expand">False</property>
2497                             <property name="fill">False</property>
2498                             <property name="position">1</property>
2499                           </packing>
2500                         </child>
2501                       </widget>
2502                     </child>
2503                   </widget>
2504                 </child>
2505               </widget>
2506               <packing>
2507                 <property name="expand">False</property>
2508                 <property name="fill">False</property>
2509                 <property name="position">2</property>
2510               </packing>
2511             </child>
2512             <child>
2513               <widget class="GtkButton" id="cancelButton">
2514                 <property name="visible">True</property>
2515                 <property name="can_focus">True</property>
2516                 <property name="label">gtk-cancel</property>
2517                 <property name="use_stock">True</property>
2518                 <property name="response_id">0</property>
2519               </widget>
2520               <packing>
2521                 <property name="expand">False</property>
2522                 <property name="fill">False</property>
2523                 <property name="position">3</property>
2524               </packing>
2525             </child>
2526           </widget>
2527           <packing>
2528             <property name="right_attach">2</property>
2529             <property name="top_attach">2</property>
2530             <property name="bottom_attach">3</property>
2531             <property name="y_padding">5</property>
2532           </packing>
2533         </child>
2534         <child>
2535           <widget class="GtkEntry" id="replaceEntry">
2536             <property name="visible">True</property>
2537             <property name="can_focus">True</property>
2538             <property name="invisible_char">*</property>
2539           </widget>
2540           <packing>
2541             <property name="left_attach">1</property>
2542             <property name="right_attach">2</property>
2543             <property name="top_attach">1</property>
2544             <property name="bottom_attach">2</property>
2545             <property name="y_options"></property>
2546           </packing>
2547         </child>
2548         <child>
2549           <widget class="GtkEntry" id="findEntry">
2550             <property name="visible">True</property>
2551             <property name="can_focus">True</property>
2552             <property name="has_focus">True</property>
2553             <property name="can_default">True</property>
2554             <property name="has_default">True</property>
2555             <property name="invisible_char">*</property>
2556           </widget>
2557           <packing>
2558             <property name="left_attach">1</property>
2559             <property name="right_attach">2</property>
2560             <property name="y_options"></property>
2561           </packing>
2562         </child>
2563         <child>
2564           <widget class="GtkLabel" id="label18">
2565             <property name="visible">True</property>
2566             <property name="xalign">0</property>
2567             <property name="label" translatable="yes">Replace with: </property>
2568           </widget>
2569           <packing>
2570             <property name="top_attach">1</property>
2571             <property name="bottom_attach">2</property>
2572             <property name="x_options">GTK_FILL</property>
2573             <property name="y_options"></property>
2574           </packing>
2575         </child>
2576         <child>
2577           <widget class="GtkLabel" id="label17">
2578             <property name="visible">True</property>
2579             <property name="xalign">0</property>
2580             <property name="label" translatable="yes">Find:</property>
2581           </widget>
2582           <packing>
2583             <property name="x_options">GTK_FILL</property>
2584             <property name="y_options"></property>
2585           </packing>
2586         </child>
2587       </widget>
2588     </child>
2589   </widget>
2590   <widget class="GtkWindow" id="NewDevelWin">
2591     <property name="title" translatable="yes">Create development</property>
2592     <property name="resizable">False</property>
2593     <property name="modal">True</property>
2594     <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
2595     <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
2596     <child>
2597       <widget class="GtkVBox" id="vbox10">
2598         <property name="visible">True</property>
2599         <child>
2600           <widget class="GtkTable" id="table2">
2601             <property name="visible">True</property>
2602             <property name="border_width">3</property>
2603             <property name="n_rows">2</property>
2604             <property name="n_columns">3</property>
2605             <property name="column_spacing">5</property>
2606             <property name="row_spacing">5</property>
2607             <child>
2608               <placeholder/>
2609             </child>
2610             <child>
2611               <widget class="GtkButton" id="chooseRootButton">
2612                 <property name="visible">True</property>
2613                 <property name="can_focus">True</property>
2614                 <property name="label" translatable="yes">...</property>
2615                 <property name="use_underline">True</property>
2616                 <property name="response_id">0</property>
2617               </widget>
2618               <packing>
2619                 <property name="left_attach">2</property>
2620                 <property name="right_attach">3</property>
2621                 <property name="top_attach">1</property>
2622                 <property name="bottom_attach">2</property>
2623                 <property name="x_options">GTK_FILL</property>
2624                 <property name="y_options"></property>
2625               </packing>
2626             </child>
2627             <child>
2628               <widget class="GtkEntry" id="rootEntry">
2629                 <property name="visible">True</property>
2630                 <property name="can_focus">True</property>
2631                 <property name="invisible_char">*</property>
2632               </widget>
2633               <packing>
2634                 <property name="left_attach">1</property>
2635                 <property name="right_attach">2</property>
2636                 <property name="top_attach">1</property>
2637                 <property name="bottom_attach">2</property>
2638                 <property name="y_options"></property>
2639               </packing>
2640             </child>
2641             <child>
2642               <widget class="GtkEntry" id="nameEntry">
2643                 <property name="visible">True</property>
2644                 <property name="can_focus">True</property>
2645                 <property name="invisible_char">*</property>
2646               </widget>
2647               <packing>
2648                 <property name="left_attach">1</property>
2649                 <property name="right_attach">2</property>
2650                 <property name="y_options"></property>
2651               </packing>
2652             </child>
2653             <child>
2654               <widget class="GtkLabel" id="label21">
2655                 <property name="visible">True</property>
2656                 <property name="xalign">0</property>
2657                 <property name="label" translatable="yes">Root directory</property>
2658               </widget>
2659               <packing>
2660                 <property name="top_attach">1</property>
2661                 <property name="bottom_attach">2</property>
2662                 <property name="x_options">GTK_FILL</property>
2663                 <property name="y_options"></property>
2664               </packing>
2665             </child>
2666             <child>
2667               <widget class="GtkLabel" id="label20">
2668                 <property name="visible">True</property>
2669                 <property name="xalign">0</property>
2670                 <property name="label" translatable="yes">Name</property>
2671               </widget>
2672               <packing>
2673                 <property name="x_options">GTK_FILL</property>
2674                 <property name="y_options"></property>
2675               </packing>
2676             </child>
2677           </widget>
2678           <packing>
2679             <property name="expand">False</property>
2680           </packing>
2681         </child>
2682         <child>
2683           <widget class="GtkHSeparator" id="hseparator1">
2684             <property name="visible">True</property>
2685           </widget>
2686           <packing>
2687             <property name="expand">False</property>
2688             <property name="padding">2</property>
2689             <property name="position">1</property>
2690           </packing>
2691         </child>
2692         <child>
2693           <widget class="GtkHBox" id="hbox21">
2694             <property name="visible">True</property>
2695             <property name="border_width">3</property>
2696             <property name="spacing">5</property>
2697             <child>
2698               <widget class="GtkVBox" id="vbox11">
2699                 <property name="visible">True</property>
2700                 <child>
2701                   <placeholder/>
2702                 </child>
2703                 <child>
2704                   <placeholder/>
2705                 </child>
2706               </widget>
2707             </child>
2708             <child>
2709               <widget class="GtkButton" id="addButton">
2710                 <property name="visible">True</property>
2711                 <property name="can_focus">True</property>
2712                 <property name="label">gtk-add</property>
2713                 <property name="use_stock">True</property>
2714                 <property name="response_id">0</property>
2715               </widget>
2716               <packing>
2717                 <property name="expand">False</property>
2718                 <property name="fill">False</property>
2719                 <property name="position">1</property>
2720               </packing>
2721             </child>
2722             <child>
2723               <widget class="GtkButton" id="cancelButton">
2724                 <property name="visible">True</property>
2725                 <property name="can_focus">True</property>
2726                 <property name="label">gtk-cancel</property>
2727                 <property name="use_stock">True</property>
2728                 <property name="response_id">0</property>
2729               </widget>
2730               <packing>
2731                 <property name="expand">False</property>
2732                 <property name="fill">False</property>
2733                 <property name="position">2</property>
2734               </packing>
2735             </child>
2736           </widget>
2737           <packing>
2738             <property name="expand">False</property>
2739             <property name="position">2</property>
2740           </packing>
2741         </child>
2742       </widget>
2743     </child>
2744   </widget>
2745   <widget class="GtkWindow" id="DevelListWin">
2746     <property name="title" translatable="yes">Developments</property>
2747     <property name="window_position">GTK_WIN_POS_CENTER</property>
2748     <child>
2749       <widget class="GtkVBox" id="vbox12">
2750         <property name="visible">True</property>
2751         <child>
2752           <widget class="GtkScrolledWindow" id="scrolledwindow10">
2753             <property name="visible">True</property>
2754             <property name="can_focus">True</property>
2755             <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2756             <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2757             <property name="shadow_type">GTK_SHADOW_IN</property>
2758             <child>
2759               <widget class="GtkTreeView" id="developmentsTreeview">
2760                 <property name="visible">True</property>
2761                 <property name="can_focus">True</property>
2762                 <property name="headers_visible">False</property>
2763               </widget>
2764             </child>
2765           </widget>
2766         </child>
2767         <child>
2768           <widget class="GtkHSeparator" id="hseparator2">
2769             <property name="visible">True</property>
2770           </widget>
2771           <packing>
2772             <property name="expand">False</property>
2773             <property name="padding">2</property>
2774             <property name="position">1</property>
2775           </packing>
2776         </child>
2777         <child>
2778           <widget class="GtkHBox" id="buttonsHbox">
2779             <property name="visible">True</property>
2780             <property name="border_width">3</property>
2781             <property name="spacing">4</property>
2782             <child>
2783               <widget class="GtkVBox" id="vbox13">
2784                 <property name="visible">True</property>
2785                 <child>
2786                   <placeholder/>
2787                 </child>
2788                 <child>
2789                   <placeholder/>
2790                 </child>
2791               </widget>
2792             </child>
2793             <child>
2794               <widget class="GtkButton" id="newButton">
2795                 <property name="visible">True</property>
2796                 <property name="can_focus">True</property>
2797                 <property name="label">gtk-new</property>
2798                 <property name="use_stock">True</property>
2799                 <property name="response_id">0</property>
2800               </widget>
2801               <packing>
2802                 <property name="expand">False</property>
2803                 <property name="fill">False</property>
2804                 <property name="position">1</property>
2805               </packing>
2806             </child>
2807             <child>
2808               <widget class="GtkButton" id="deleteButton">
2809                 <property name="visible">True</property>
2810                 <property name="can_focus">True</property>
2811                 <property name="label">gtk-delete</property>
2812                 <property name="use_stock">True</property>
2813                 <property name="response_id">0</property>
2814               </widget>
2815               <packing>
2816                 <property name="expand">False</property>
2817                 <property name="fill">False</property>
2818                 <property name="position">2</property>
2819               </packing>
2820             </child>
2821             <child>
2822               <widget class="GtkButton" id="buildButton">
2823                 <property name="visible">True</property>
2824                 <property name="can_focus">True</property>
2825                 <property name="response_id">0</property>
2826                 <child>
2827                   <widget class="GtkAlignment" id="alignment14">
2828                     <property name="visible">True</property>
2829                     <property name="xscale">0</property>
2830                     <property name="yscale">0</property>
2831                     <child>
2832                       <widget class="GtkHBox" id="hbox23">
2833                         <property name="visible">True</property>
2834                         <property name="spacing">2</property>
2835                         <child>
2836                           <widget class="GtkImage" id="image358">
2837                             <property name="visible">True</property>
2838                             <property name="stock">gtk-execute</property>
2839                           </widget>
2840                           <packing>
2841                             <property name="expand">False</property>
2842                             <property name="fill">False</property>
2843                           </packing>
2844                         </child>
2845                         <child>
2846                           <widget class="GtkLabel" id="label22">
2847                             <property name="visible">True</property>
2848                             <property name="label" translatable="yes">_Build</property>
2849                             <property name="use_underline">True</property>
2850                           </widget>
2851                           <packing>
2852                             <property name="expand">False</property>
2853                             <property name="fill">False</property>
2854                             <property name="position">1</property>
2855                           </packing>
2856                         </child>
2857                       </widget>
2858                     </child>
2859                   </widget>
2860                 </child>
2861               </widget>
2862               <packing>
2863                 <property name="expand">False</property>
2864                 <property name="fill">False</property>
2865                 <property name="position">3</property>
2866               </packing>
2867             </child>
2868             <child>
2869               <widget class="GtkButton" id="cleanButton">
2870                 <property name="visible">True</property>
2871                 <property name="can_focus">True</property>
2872                 <property name="response_id">0</property>
2873                 <child>
2874                   <widget class="GtkAlignment" id="alignment15">
2875                     <property name="visible">True</property>
2876                     <property name="xscale">0</property>
2877                     <property name="yscale">0</property>
2878                     <child>
2879                       <widget class="GtkHBox" id="hbox24">
2880                         <property name="visible">True</property>
2881                         <property name="spacing">2</property>
2882                         <child>
2883                           <widget class="GtkImage" id="image359">
2884                             <property name="visible">True</property>
2885                             <property name="stock">gtk-clear</property>
2886                           </widget>
2887                           <packing>
2888                             <property name="expand">False</property>
2889                             <property name="fill">False</property>
2890                           </packing>
2891                         </child>
2892                         <child>
2893                           <widget class="GtkLabel" id="label23">
2894                             <property name="visible">True</property>
2895                             <property name="label" translatable="yes">C_lean</property>
2896                             <property name="use_underline">True</property>
2897                           </widget>
2898                           <packing>
2899                             <property name="expand">False</property>
2900                             <property name="fill">False</property>
2901                             <property name="position">1</property>
2902                           </packing>
2903                         </child>
2904                       </widget>
2905                     </child>
2906                   </widget>
2907                 </child>
2908               </widget>
2909               <packing>
2910                 <property name="expand">False</property>
2911                 <property name="fill">False</property>
2912                 <property name="position">4</property>
2913               </packing>
2914             </child>
2915             <child>
2916               <widget class="GtkButton" id="publishButton">
2917                 <property name="visible">True</property>
2918                 <property name="can_focus">True</property>
2919                 <property name="response_id">0</property>
2920                 <child>
2921                   <widget class="GtkAlignment" id="alignment16">
2922                     <property name="visible">True</property>
2923                     <property name="xscale">0</property>
2924                     <property name="yscale">0</property>
2925                     <child>
2926                       <widget class="GtkHBox" id="hbox25">
2927                         <property name="visible">True</property>
2928                         <property name="spacing">2</property>
2929                         <child>
2930                           <widget class="GtkImage" id="image907">
2931                             <property name="visible">True</property>
2932                             <property name="stock">gtk-convert</property>
2933                           </widget>
2934                           <packing>
2935                             <property name="expand">False</property>
2936                             <property name="fill">False</property>
2937                           </packing>
2938                         </child>
2939                         <child>
2940                           <widget class="GtkLabel" id="label24">
2941                             <property name="visible">True</property>
2942                             <property name="label" translatable="yes">Publish</property>
2943                             <property name="use_underline">True</property>
2944                           </widget>
2945                           <packing>
2946                             <property name="expand">False</property>
2947                             <property name="fill">False</property>
2948                             <property name="position">1</property>
2949                           </packing>
2950                         </child>
2951                       </widget>
2952                     </child>
2953                   </widget>
2954                 </child>
2955               </widget>
2956               <packing>
2957                 <property name="expand">False</property>
2958                 <property name="fill">False</property>
2959                 <property name="position">5</property>
2960               </packing>
2961             </child>
2962             <child>
2963               <widget class="GtkButton" id="graphButton">
2964                 <property name="visible">True</property>
2965                 <property name="can_focus">True</property>
2966                 <property name="response_id">0</property>
2967                 <child>
2968                   <widget class="GtkAlignment" id="alignment17">
2969                     <property name="visible">True</property>
2970                     <property name="xscale">0</property>
2971                     <property name="yscale">0</property>
2972                     <child>
2973                       <widget class="GtkHBox" id="hbox26">
2974                         <property name="visible">True</property>
2975                         <property name="spacing">2</property>
2976                         <child>
2977                           <widget class="GtkImage" id="image908">
2978                             <property name="visible">True</property>
2979                             <property name="stock">gtk-zoom-fit</property>
2980                           </widget>
2981                           <packing>
2982                             <property name="expand">False</property>
2983                             <property name="fill">False</property>
2984                           </packing>
2985                         </child>
2986                         <child>
2987                           <widget class="GtkLabel" id="label27">
2988                             <property name="visible">True</property>
2989                             <property name="label" translatable="yes">Graph</property>
2990                             <property name="use_underline">True</property>
2991                           </widget>
2992                           <packing>
2993                             <property name="expand">False</property>
2994                             <property name="fill">False</property>
2995                             <property name="position">1</property>
2996                           </packing>
2997                         </child>
2998                       </widget>
2999                     </child>
3000                   </widget>
3001                 </child>
3002               </widget>
3003               <packing>
3004                 <property name="expand">False</property>
3005                 <property name="fill">False</property>
3006                 <property name="position">6</property>
3007               </packing>
3008             </child>
3009             <child>
3010               <widget class="GtkButton" id="closeButton">
3011                 <property name="visible">True</property>
3012                 <property name="can_focus">True</property>
3013                 <property name="label">gtk-close</property>
3014                 <property name="use_stock">True</property>
3015                 <property name="response_id">0</property>
3016               </widget>
3017               <packing>
3018                 <property name="expand">False</property>
3019                 <property name="fill">False</property>
3020                 <property name="position">7</property>
3021               </packing>
3022             </child>
3023           </widget>
3024           <packing>
3025             <property name="expand">False</property>
3026             <property name="position">2</property>
3027           </packing>
3028         </child>
3029       </widget>
3030     </child>
3031   </widget>
3032   <widget class="GtkDialog" id="DisambiguationErrors">
3033     <property name="width_request">450</property>
3034     <property name="height_request">400</property>
3035     <property name="title" translatable="yes">title</property>
3036     <property name="modal">True</property>
3037     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3038     <child internal-child="vbox">
3039       <widget class="GtkVBox" id="vbox14">
3040         <property name="visible">True</property>
3041         <child>
3042           <widget class="GtkVBox" id="vbox15">
3043             <property name="visible">True</property>
3044             <child>
3045               <widget class="GtkLabel" id="disambiguationErrorsLabel">
3046                 <property name="visible">True</property>
3047                 <property name="label" translatable="yes">some informative message here ...</property>
3048               </widget>
3049               <packing>
3050                 <property name="expand">False</property>
3051                 <property name="fill">False</property>
3052               </packing>
3053             </child>
3054             <child>
3055               <widget class="GtkScrolledWindow" id="scrolledwindow12">
3056                 <property name="visible">True</property>
3057                 <property name="can_focus">True</property>
3058                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3059                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3060                 <property name="shadow_type">GTK_SHADOW_IN</property>
3061                 <child>
3062                   <widget class="GtkTreeView" id="treeview">
3063                     <property name="visible">True</property>
3064                     <property name="can_focus">True</property>
3065                     <property name="headers_visible">False</property>
3066                   </widget>
3067                 </child>
3068               </widget>
3069               <packing>
3070                 <property name="position">1</property>
3071               </packing>
3072             </child>
3073           </widget>
3074           <packing>
3075             <property name="position">2</property>
3076           </packing>
3077         </child>
3078         <child internal-child="action_area">
3079           <widget class="GtkHButtonBox" id="hbuttonbox2">
3080             <property name="visible">True</property>
3081             <property name="layout_style">GTK_BUTTONBOX_END</property>
3082             <child>
3083               <widget class="GtkButton" id="button6">
3084                 <property name="visible">True</property>
3085                 <property name="can_focus">True</property>
3086                 <property name="can_default">True</property>
3087                 <property name="label">gtk-help</property>
3088                 <property name="use_stock">True</property>
3089                 <property name="response_id">-11</property>
3090               </widget>
3091             </child>
3092             <child>
3093               <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
3094                 <property name="visible">True</property>
3095                 <property name="can_focus">True</property>
3096                 <property name="can_default">True</property>
3097                 <property name="response_id">-6</property>
3098                 <child>
3099                   <widget class="GtkAlignment" id="alignment18">
3100                     <property name="visible">True</property>
3101                     <property name="xscale">0</property>
3102                     <property name="yscale">0</property>
3103                     <child>
3104                       <widget class="GtkHBox" id="hbox29">
3105                         <property name="visible">True</property>
3106                         <property name="spacing">2</property>
3107                         <child>
3108                           <widget class="GtkImage" id="image926">
3109                             <property name="visible">True</property>
3110                             <property name="stock">gtk-zoom-in</property>
3111                           </widget>
3112                           <packing>
3113                             <property name="expand">False</property>
3114                             <property name="fill">False</property>
3115                           </packing>
3116                         </child>
3117                         <child>
3118                           <widget class="GtkLabel" id="label28">
3119                             <property name="visible">True</property>
3120                             <property name="label">More</property>
3121                             <property name="use_underline">True</property>
3122                           </widget>
3123                           <packing>
3124                             <property name="expand">False</property>
3125                             <property name="fill">False</property>
3126                             <property name="position">1</property>
3127                           </packing>
3128                         </child>
3129                       </widget>
3130                     </child>
3131                   </widget>
3132                 </child>
3133               </widget>
3134               <packing>
3135                 <property name="position">1</property>
3136               </packing>
3137             </child>
3138             <child>
3139               <widget class="GtkButton" id="disambiguationErrorsCancelButton">
3140                 <property name="visible">True</property>
3141                 <property name="can_focus">True</property>
3142                 <property name="can_default">True</property>
3143                 <property name="has_default">True</property>
3144                 <property name="label">gtk-cancel</property>
3145                 <property name="use_stock">True</property>
3146                 <property name="response_id">-6</property>
3147               </widget>
3148               <packing>
3149                 <property name="position">2</property>
3150               </packing>
3151             </child>
3152             <child>
3153               <widget class="GtkButton" id="disambiguationErrorsOkButton">
3154                 <property name="visible">True</property>
3155                 <property name="can_focus">True</property>
3156                 <property name="can_default">True</property>
3157                 <property name="label">gtk-ok</property>
3158                 <property name="use_stock">True</property>
3159                 <property name="response_id">-5</property>
3160               </widget>
3161               <packing>
3162                 <property name="position">3</property>
3163               </packing>
3164             </child>
3165           </widget>
3166           <packing>
3167             <property name="expand">False</property>
3168             <property name="pack_type">GTK_PACK_END</property>
3169           </packing>
3170         </child>
3171       </widget>
3172     </child>
3173   </widget>
3174   <widget class="GtkWindow" id="AutoWin">
3175     <property name="width_request">600</property>
3176     <property name="height_request">400</property>
3177     <property name="visible">True</property>
3178     <property name="title" translatable="yes">Auto</property>
3179     <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3180     <property name="gravity">GDK_GRAVITY_SOUTH_EAST</property>
3181     <child>
3182       <widget class="GtkVBox" id="vbox17">
3183         <property name="visible">True</property>
3184         <child>
3185           <widget class="GtkHBox" id="hbox30">
3186             <property name="visible">True</property>
3187             <property name="spacing">2</property>
3188             <child>
3189               <widget class="GtkScrolledWindow" id="scrolledwindowAREA">
3190                 <property name="visible">True</property>
3191                 <property name="can_focus">True</property>
3192                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3193                 <property name="shadow_type">GTK_SHADOW_IN</property>
3194                 <child>
3195                   <widget class="GtkViewport" id="viewportAREA">
3196                     <property name="visible">True</property>
3197                     <child>
3198                       <widget class="GtkTable" id="table">
3199                         <property name="visible">True</property>
3200                         <property name="n_rows">3</property>
3201                         <property name="n_columns">3</property>
3202                         <child>
3203                           <placeholder/>
3204                         </child>
3205                         <child>
3206                           <placeholder/>
3207                         </child>
3208                         <child>
3209                           <placeholder/>
3210                         </child>
3211                         <child>
3212                           <placeholder/>
3213                         </child>
3214                         <child>
3215                           <placeholder/>
3216                         </child>
3217                         <child>
3218                           <placeholder/>
3219                         </child>
3220                         <child>
3221                           <placeholder/>
3222                         </child>
3223                         <child>
3224                           <placeholder/>
3225                         </child>
3226                         <child>
3227                           <placeholder/>
3228                         </child>
3229                       </widget>
3230                     </child>
3231                   </widget>
3232                 </child>
3233               </widget>
3234             </child>
3235             <child>
3236               <widget class="GtkVBox" id="vbox18">
3237                 <property name="visible">True</property>
3238                 <child>
3239                   <widget class="GtkButton" id="buttonUP">
3240                     <property name="visible">True</property>
3241                     <property name="can_focus">True</property>
3242                     <property name="response_id">0</property>
3243                     <child>
3244                       <widget class="GtkAlignment" id="alignment19">
3245                         <property name="visible">True</property>
3246                         <property name="xscale">0</property>
3247                         <property name="yscale">0</property>
3248                         <child>
3249                           <widget class="GtkHBox" id="hbox31">
3250                             <property name="visible">True</property>
3251                             <property name="spacing">2</property>
3252                             <child>
3253                               <widget class="GtkImage" id="image1066">
3254                                 <property name="visible">True</property>
3255                                 <property name="stock">gtk-go-up</property>
3256                               </widget>
3257                               <packing>
3258                                 <property name="expand">False</property>
3259                                 <property name="fill">False</property>
3260                               </packing>
3261                             </child>
3262                             <child>
3263                               <widget class="GtkLabel" id="label30">
3264                                 <property name="visible">True</property>
3265                                 <property name="use_underline">True</property>
3266                               </widget>
3267                               <packing>
3268                                 <property name="expand">False</property>
3269                                 <property name="fill">False</property>
3270                                 <property name="position">1</property>
3271                               </packing>
3272                             </child>
3273                           </widget>
3274                         </child>
3275                       </widget>
3276                     </child>
3277                   </widget>
3278                 </child>
3279                 <child>
3280                   <widget class="GtkButton" id="buttonDOWN">
3281                     <property name="visible">True</property>
3282                     <property name="can_focus">True</property>
3283                     <property name="response_id">0</property>
3284                     <child>
3285                       <widget class="GtkImage" id="image1065">
3286                         <property name="visible">True</property>
3287                         <property name="stock">gtk-go-down</property>
3288                       </widget>
3289                     </child>
3290                   </widget>
3291                   <packing>
3292                     <property name="position">1</property>
3293                   </packing>
3294                 </child>
3295               </widget>
3296               <packing>
3297                 <property name="expand">False</property>
3298                 <property name="fill">False</property>
3299                 <property name="position">1</property>
3300               </packing>
3301             </child>
3302           </widget>
3303         </child>
3304         <child>
3305           <widget class="GtkHSeparator" id="hseparator3">
3306             <property name="visible">True</property>
3307           </widget>
3308           <packing>
3309             <property name="expand">False</property>
3310             <property name="padding">3</property>
3311             <property name="position">1</property>
3312           </packing>
3313         </child>
3314         <child>
3315           <widget class="GtkHBox" id="hbox32">
3316             <property name="visible">True</property>
3317             <child>
3318               <widget class="GtkLabel" id="labelLAST">
3319                 <property name="visible">True</property>
3320                 <property name="xalign">0</property>
3321                 <property name="label" translatable="yes">Last:</property>
3322               </widget>
3323             </child>
3324             <child>
3325               <widget class="GtkHButtonBox" id="hbuttonbox3">
3326                 <property name="visible">True</property>
3327                 <property name="border_width">4</property>
3328                 <property name="spacing">4</property>
3329                 <property name="layout_style">GTK_BUTTONBOX_END</property>
3330                 <child>
3331                   <widget class="GtkButton" id="buttonPAUSE">
3332                     <property name="visible">True</property>
3333                     <property name="can_focus">True</property>
3334                     <property name="can_default">True</property>
3335                     <property name="label">gtk-media-pause</property>
3336                     <property name="use_stock">True</property>
3337                     <property name="response_id">0</property>
3338                   </widget>
3339                 </child>
3340                 <child>
3341                   <widget class="GtkButton" id="buttonPLAY">
3342                     <property name="visible">True</property>
3343                     <property name="can_focus">True</property>
3344                     <property name="can_default">True</property>
3345                     <property name="label">gtk-media-play</property>
3346                     <property name="use_stock">True</property>
3347                     <property name="response_id">0</property>
3348                   </widget>
3349                   <packing>
3350                     <property name="position">1</property>
3351                   </packing>
3352                 </child>
3353                 <child>
3354                   <widget class="GtkButton" id="buttonNEXT">
3355                     <property name="visible">True</property>
3356                     <property name="can_focus">True</property>
3357                     <property name="can_default">True</property>
3358                     <property name="label">gtk-media-next</property>
3359                     <property name="use_stock">True</property>
3360                     <property name="response_id">0</property>
3361                   </widget>
3362                   <packing>
3363                     <property name="position">2</property>
3364                   </packing>
3365                 </child>
3366                 <child>
3367                   <widget class="GtkButton" id="buttonCLOSE">
3368                     <property name="visible">True</property>
3369                     <property name="can_focus">True</property>
3370                     <property name="can_default">True</property>
3371                     <property name="label">gtk-close</property>
3372                     <property name="use_stock">True</property>
3373                     <property name="response_id">0</property>
3374                   </widget>
3375                   <packing>
3376                     <property name="position">3</property>
3377                   </packing>
3378                 </child>
3379               </widget>
3380               <packing>
3381                 <property name="position">1</property>
3382               </packing>
3383             </child>
3384           </widget>
3385           <packing>
3386             <property name="expand">False</property>
3387             <property name="position">2</property>
3388           </packing>
3389         </child>
3390       </widget>
3391     </child>
3392   </widget>
3393 </glade-interface>