helm/software/matita/matita.glade

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