helm/software/matita/matita.glade

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