matita/matita.glade

   1 <?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
   2 <!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
   3
   4 <glade-interface>
   5
   6 <widget class="GtkWindow" id="BrowserWin">
   7   <property name="visible">True</property>
   8   <property name="title" translatable="yes">Cic browser</property>
   9   <property name="type">GTK_WINDOW_TOPLEVEL</property>
  10   <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
  11   <property name="modal">False</property>
  12   <property name="default_width">500</property>
  13   <property name="default_height">500</property>
  14   <property name="resizable">True</property>
  15   <property name="destroy_with_parent">False</property>
  16   <property name="decorated">True</property>
  17   <property name="skip_taskbar_hint">False</property>
  18   <property name="skip_pager_hint">False</property>
  19   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
  20   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
  21   <property name="focus_on_map">True</property>
  22   <property name="urgency_hint">False</property>
  23
  24   <child>
  25     <widget class="GtkEventBox" id="BrowserWinEventBox">
  26       <property name="visible">True</property>
  27       <property name="visible_window">True</property>
  28       <property name="above_child">False</property>
  29
  30       <child>
  31         <widget class="GtkVBox" id="BrowserVBox">
  32           <property name="visible">True</property>
  33           <property name="homogeneous">False</property>
  34           <property name="spacing">0</property>
  35
  36           <child>
  37             <widget class="GtkMenuBar" id="menubar2">
  38               <property name="visible">True</property>
  39               <property name="pack_direction">GTK_PACK_DIRECTION_LTR</property>
  40               <property name="child_pack_direction">GTK_PACK_DIRECTION_LTR</property>
  41
  42               <child>
  43                 <widget class="GtkMenuItem" id="BrowserFileMenu">
  44                   <property name="visible">True</property>
  45                   <property name="label" translatable="yes">_File</property>
  46                   <property name="use_underline">True</property>
  47
  48                   <child>
  49                     <widget class="GtkMenu" id="BrowserFileMenu_menu">
  50
  51                       <child>
  52                         <widget class="GtkImageMenuItem" id="BrowserNewMenuItem">
  53                           <property name="visible">True</property>
  54                           <property name="label">gtk-new</property>
  55                           <property name="use_stock">True</property>
  56                         </widget>
  57                       </child>
  58
  59                       <child>
  60                         <widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
  61                           <property name="visible">True</property>
  62                         </widget>
  63                       </child>
  64
  65                       <child>
  66                         <widget class="GtkImageMenuItem" id="BrowserCloseMenuItem">
  67                           <property name="visible">True</property>
  68                           <property name="label">gtk-close</property>
  69                           <property name="use_stock">True</property>
  70                         </widget>
  71                       </child>
  72                     </widget>
  73                   </child>
  74                 </widget>
  75               </child>
  76
  77               <child>
  78                 <widget class="GtkMenuItem" id="BrowserEditMenu">
  79                   <property name="visible">True</property>
  80                   <property name="label" translatable="yes">_Edit</property>
  81                   <property name="use_underline">True</property>
  82
  83                   <child>
  84                     <widget class="GtkMenu" id="BrowserEditMenu_menu">
  85
  86                       <child>
  87                         <widget class="GtkImageMenuItem" id="BrowserCopyMenuItem">
  88                           <property name="visible">True</property>
  89                           <property name="label">gtk-copy</property>
  90                           <property name="use_stock">True</property>
  91                         </widget>
  92                       </child>
  93                     </widget>
  94                   </child>
  95                 </widget>
  96               </child>
  97
  98               <child>
  99                 <widget class="GtkMenuItem" id="BrowserViewMenu">
 100                   <property name="visible">True</property>
 101                   <property name="label" translatable="yes">_View</property>
 102                   <property name="use_underline">True</property>
 103
 104                   <child>
 105                     <widget class="GtkMenu" id="BrowserViewMenu_menu">
 106
 107                       <child>
 108                         <widget class="GtkMenuItem" id="BrowserMetadataMenuItem">
 109                           <property name="visible">True</property>
 110                           <property name="label" translatable="yes">_Metadata</property>
 111                           <property name="use_underline">True</property>
 112                         </widget>
 113                       </child>
 114
 115                       <child>
 116                         <widget class="GtkMenuItem" id="DepGraphMenuItem">
 117                           <property name="visible">True</property>
 118                           <property name="tooltip" translatable="yes">View the graph of objects on which the current one depends on</property>
 119                           <property name="label" translatable="yes">(Direct) Dependencies</property>
 120                           <property name="use_underline">True</property>
 121                         </widget>
 122                       </child>
 123
 124                       <child>
 125                         <widget class="GtkMenuItem" id="InvDepGraphMenuItem">
 126                           <property name="visible">True</property>
 127                           <property name="tooltip" translatable="yes">View the graph of objects which depends on the current one</property>
 128                           <property name="label" translatable="yes">(Inverse) Dependencies</property>
 129                           <property name="use_underline">True</property>
 130                         </widget>
 131                       </child>
 132                     </widget>
 133                   </child>
 134                 </widget>
 135               </child>
 136             </widget>
 137             <packing>
 138               <property name="padding">0</property>
 139               <property name="expand">False</property>
 140               <property name="fill">False</property>
 141             </packing>
 142           </child>
 143
 144           <child>
 145             <widget class="GtkFrame" id="frame2">
 146               <property name="visible">True</property>
 147               <property name="label_xalign">0</property>
 148               <property name="label_yalign">0</property>
 149               <property name="shadow_type">GTK_SHADOW_NONE</property>
 150
 151               <child>
 152                 <widget class="GtkHBox" id="BrowserHBox">
 153                   <property name="visible">True</property>
 154                   <property name="homogeneous">False</property>
 155                   <property name="spacing">0</property>
 156
 157                   <child>
 158                     <widget class="GtkButton" id="BrowserNewButton">
 159                       <property name="visible">True</property>
 160                       <property name="can_focus">True</property>
 161                       <property name="relief">GTK_RELIEF_NONE</property>
 162                       <property name="focus_on_click">True</property>
 163
 164                       <child>
 165                         <widget class="GtkImage" id="image303">
 166                           <property name="visible">True</property>
 167                           <property name="stock">gtk-new</property>
 168                           <property name="icon_size">4</property>
 169                           <property name="xalign">0.5</property>
 170                           <property name="yalign">0.5</property>
 171                           <property name="xpad">0</property>
 172                           <property name="ypad">0</property>
 173                         </widget>
 174                       </child>
 175                     </widget>
 176                     <packing>
 177                       <property name="padding">0</property>
 178                       <property name="expand">False</property>
 179                       <property name="fill">False</property>
 180                     </packing>
 181                   </child>
 182
 183                   <child>
 184                     <widget class="GtkButton" id="BrowserBackButton">
 185                       <property name="visible">True</property>
 186                       <property name="can_focus">True</property>
 187                       <property name="relief">GTK_RELIEF_NONE</property>
 188                       <property name="focus_on_click">True</property>
 189
 190                       <child>
 191                         <widget class="GtkImage" id="image304">
 192                           <property name="visible">True</property>
 193                           <property name="stock">gtk-go-back</property>
 194                           <property name="icon_size">4</property>
 195                           <property name="xalign">0.5</property>
 196                           <property name="yalign">0.5</property>
 197                           <property name="xpad">0</property>
 198                           <property name="ypad">0</property>
 199                         </widget>
 200                       </child>
 201                     </widget>
 202                     <packing>
 203                       <property name="padding">0</property>
 204                       <property name="expand">False</property>
 205                       <property name="fill">False</property>
 206                     </packing>
 207                   </child>
 208
 209                   <child>
 210                     <widget class="GtkButton" id="BrowserForwardButton">
 211                       <property name="visible">True</property>
 212                       <property name="can_focus">True</property>
 213                       <property name="relief">GTK_RELIEF_NONE</property>
 214                       <property name="focus_on_click">True</property>
 215
 216                       <child>
 217                         <widget class="GtkImage" id="image305">
 218                           <property name="visible">True</property>
 219                           <property name="stock">gtk-go-forward</property>
 220                           <property name="icon_size">4</property>
 221                           <property name="xalign">0.5</property>
 222                           <property name="yalign">0.5</property>
 223                           <property name="xpad">0</property>
 224                           <property name="ypad">0</property>
 225                         </widget>
 226                       </child>
 227                     </widget>
 228                     <packing>
 229                       <property name="padding">0</property>
 230                       <property name="expand">False</property>
 231                       <property name="fill">False</property>
 232                     </packing>
 233                   </child>
 234
 235                   <child>
 236                     <widget class="GtkButton" id="BrowserRefreshButton">
 237                       <property name="visible">True</property>
 238                       <property name="tooltip" translatable="yes">refresh</property>
 239                       <property name="can_default">True</property>
 240                       <property name="can_focus">True</property>
 241                       <property name="relief">GTK_RELIEF_NONE</property>
 242                       <property name="focus_on_click">True</property>
 243
 244                       <child>
 245                         <widget class="GtkImage" id="image229">
 246                           <property name="visible">True</property>
 247                           <property name="stock">gtk-refresh</property>
 248                           <property name="icon_size">4</property>
 249                           <property name="xalign">0.5</property>
 250                           <property name="yalign">0.5</property>
 251                           <property name="xpad">0</property>
 252                           <property name="ypad">0</property>
 253                         </widget>
 254                       </child>
 255                     </widget>
 256                     <packing>
 257                       <property name="padding">0</property>
 258                       <property name="expand">False</property>
 259                       <property name="fill">False</property>
 260                     </packing>
 261                   </child>
 262
 263                   <child>
 264                     <widget class="GtkButton" id="BrowserHomeButton">
 265                       <property name="visible">True</property>
 266                       <property name="tooltip" translatable="yes">home</property>
 267                       <property name="can_default">True</property>
 268                       <property name="can_focus">True</property>
 269                       <property name="relief">GTK_RELIEF_NONE</property>
 270                       <property name="focus_on_click">True</property>
 271
 272                       <child>
 273                         <widget class="GtkImage" id="image190">
 274                           <property name="visible">True</property>
 275                           <property name="stock">gtk-home</property>
 276                           <property name="icon_size">4</property>
 277                           <property name="xalign">0.5</property>
 278                           <property name="yalign">0.5</property>
 279                           <property name="xpad">0</property>
 280                           <property name="ypad">0</property>
 281                         </widget>
 282                       </child>
 283                     </widget>
 284                     <packing>
 285                       <property name="padding">0</property>
 286                       <property name="expand">False</property>
 287                       <property name="fill">False</property>
 288                     </packing>
 289                   </child>
 290
 291                   <child>
 292                     <widget class="GtkImage" id="image301">
 293                       <property name="visible">True</property>
 294                       <property name="stock">gtk-jump-to</property>
 295                       <property name="icon_size">2</property>
 296                       <property name="xalign">0.5</property>
 297                       <property name="yalign">0.5</property>
 298                       <property name="xpad">0</property>
 299                       <property name="ypad">0</property>
 300                     </widget>
 301                     <packing>
 302                       <property name="padding">3</property>
 303                       <property name="expand">False</property>
 304                       <property name="fill">False</property>
 305                     </packing>
 306                   </child>
 307
 308                   <child>
 309                     <widget class="GtkHBox" id="UriHBox">
 310                       <property name="visible">True</property>
 311                       <property name="homogeneous">False</property>
 312                       <property name="spacing">0</property>
 313
 314                       <child>
 315                         <placeholder/>
 316                       </child>
 317                     </widget>
 318                     <packing>
 319                       <property name="padding">0</property>
 320                       <property name="expand">True</property>
 321                       <property name="fill">True</property>
 322                     </packing>
 323                   </child>
 324                 </widget>
 325               </child>
 326             </widget>
 327             <packing>
 328               <property name="padding">0</property>
 329               <property name="expand">False</property>
 330               <property name="fill">True</property>
 331             </packing>
 332           </child>
 333
 334           <child>
 335             <widget class="GtkHBox" id="whelpBarBox">
 336               <property name="border_width">3</property>
 337               <property name="visible">True</property>
 338               <property name="homogeneous">False</property>
 339               <property name="spacing">6</property>
 340
 341               <child>
 342                 <widget class="GtkImage" id="WhelpBarImage">
 343                   <property name="visible">True</property>
 344                   <property name="xalign">0.5</property>
 345                   <property name="yalign">0.5</property>
 346                   <property name="xpad">0</property>
 347                   <property name="ypad">0</property>
 348                 </widget>
 349                 <packing>
 350                   <property name="padding">0</property>
 351                   <property name="expand">False</property>
 352                   <property name="fill">True</property>
 353                 </packing>
 354               </child>
 355
 356               <child>
 357                 <widget class="GtkEntry" id="queryInputText">
 358                   <property name="visible">True</property>
 359                   <property name="can_focus">True</property>
 360                   <property name="editable">True</property>
 361                   <property name="visibility">True</property>
 362                   <property name="max_length">0</property>
 363                   <property name="text" translatable="yes"></property>
 364                   <property name="has_frame">True</property>
 365                   <property name="invisible_char">*</property>
 366                   <property name="activates_default">False</property>
 367                 </widget>
 368                 <packing>
 369                   <property name="padding">0</property>
 370                   <property name="expand">True</property>
 371                   <property name="fill">True</property>
 372                 </packing>
 373               </child>
 374
 375               <child>
 376                 <widget class="GtkVBox" id="whelpBarComboVbox">
 377                   <property name="visible">True</property>
 378                   <property name="homogeneous">False</property>
 379                   <property name="spacing">0</property>
 380
 381                   <child>
 382                     <widget class="GtkAlignment" id="alignment4">
 383                       <property name="visible">True</property>
 384                       <property name="xalign">0.5</property>
 385                       <property name="yalign">0.5</property>
 386                       <property name="xscale">1</property>
 387                       <property name="yscale">1</property>
 388                       <property name="top_padding">0</property>
 389                       <property name="bottom_padding">0</property>
 390                       <property name="left_padding">0</property>
 391                       <property name="right_padding">0</property>
 392
 393                       <child>
 394                         <placeholder/>
 395                       </child>
 396                     </widget>
 397                     <packing>
 398                       <property name="padding">0</property>
 399                       <property name="expand">False</property>
 400                       <property name="fill">False</property>
 401                     </packing>
 402                   </child>
 403                 </widget>
 404                 <packing>
 405                   <property name="padding">0</property>
 406                   <property name="expand">False</property>
 407                   <property name="fill">True</property>
 408                 </packing>
 409               </child>
 410             </widget>
 411             <packing>
 412               <property name="padding">0</property>
 413               <property name="expand">False</property>
 414               <property name="fill">True</property>
 415             </packing>
 416           </child>
 417
 418           <child>
 419             <widget class="GtkNotebook" id="mathOrListNotebook">
 420               <property name="visible">True</property>
 421               <property name="can_focus">True</property>
 422               <property name="show_tabs">True</property>
 423               <property name="show_border">True</property>
 424               <property name="tab_pos">GTK_POS_TOP</property>
 425               <property name="scrollable">False</property>
 426               <property name="enable_popup">False</property>
 427
 428               <child>
 429                 <widget class="GtkScrolledWindow" id="ScrolledBrowser">
 430                   <property name="visible">True</property>
 431                   <property name="can_focus">True</property>
 432                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 433                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 434                   <property name="shadow_type">GTK_SHADOW_NONE</property>
 435                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 436
 437                   <child>
 438                     <placeholder/>
 439                   </child>
 440                 </widget>
 441                 <packing>
 442                   <property name="tab_expand">False</property>
 443                   <property name="tab_fill">True</property>
 444                 </packing>
 445               </child>
 446
 447               <child>
 448                 <widget class="GtkLabel" id="mathLabel">
 449                   <property name="visible">True</property>
 450                   <property name="label" translatable="yes">MathView</property>
 451                   <property name="use_underline">False</property>
 452                   <property name="use_markup">False</property>
 453                   <property name="justify">GTK_JUSTIFY_LEFT</property>
 454                   <property name="wrap">False</property>
 455                   <property name="selectable">False</property>
 456                   <property name="xalign">0.5</property>
 457                   <property name="yalign">0.5</property>
 458                   <property name="xpad">0</property>
 459                   <property name="ypad">0</property>
 460                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 461                   <property name="width_chars">-1</property>
 462                   <property name="single_line_mode">False</property>
 463                   <property name="angle">0</property>
 464                 </widget>
 465                 <packing>
 466                   <property name="type">tab</property>
 467                 </packing>
 468               </child>
 469
 470               <child>
 471                 <widget class="GtkScrolledWindow" id="scrolledwindow9">
 472                   <property name="visible">True</property>
 473                   <property name="can_focus">True</property>
 474                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 475                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 476                   <property name="shadow_type">GTK_SHADOW_IN</property>
 477                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 478
 479                   <child>
 480                     <widget class="GtkTreeView" id="whelpResultTreeview">
 481                       <property name="visible">True</property>
 482                       <property name="can_focus">True</property>
 483                       <property name="headers_visible">False</property>
 484                       <property name="rules_hint">False</property>
 485                       <property name="reorderable">False</property>
 486                       <property name="enable_search">True</property>
 487                       <property name="fixed_height_mode">False</property>
 488                       <property name="hover_selection">False</property>
 489                       <property name="hover_expand">False</property>
 490                     </widget>
 491                   </child>
 492                 </widget>
 493                 <packing>
 494                   <property name="tab_expand">False</property>
 495                   <property name="tab_fill">True</property>
 496                 </packing>
 497               </child>
 498
 499               <child>
 500                 <widget class="GtkLabel" id="listLabel">
 501                   <property name="visible">True</property>
 502                   <property name="label" translatable="yes">WhelpResults</property>
 503                   <property name="use_underline">False</property>
 504                   <property name="use_markup">False</property>
 505                   <property name="justify">GTK_JUSTIFY_LEFT</property>
 506                   <property name="wrap">False</property>
 507                   <property name="selectable">False</property>
 508                   <property name="xalign">0.5</property>
 509                   <property name="yalign">0.5</property>
 510                   <property name="xpad">0</property>
 511                   <property name="ypad">0</property>
 512                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 513                   <property name="width_chars">-1</property>
 514                   <property name="single_line_mode">False</property>
 515                   <property name="angle">0</property>
 516                 </widget>
 517                 <packing>
 518                   <property name="type">tab</property>
 519                 </packing>
 520               </child>
 521
 522               <child>
 523                 <widget class="GtkScrolledWindow" id="scrolledwindow11">
 524                   <property name="visible">True</property>
 525                   <property name="can_focus">True</property>
 526                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 527                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 528                   <property name="shadow_type">GTK_SHADOW_NONE</property>
 529                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 530
 531                   <child>
 532                     <widget class="GtkViewport" id="viewport2">
 533                       <property name="visible">True</property>
 534                       <property name="shadow_type">GTK_SHADOW_NONE</property>
 535
 536                       <child>
 537                         <widget class="GtkImage" id="BrowserImage">
 538                           <property name="visible">True</property>
 539                           <property name="xalign">0.5</property>
 540                           <property name="yalign">0.5</property>
 541                           <property name="xpad">0</property>
 542                           <property name="ypad">0</property>
 543                         </widget>
 544                       </child>
 545                     </widget>
 546                   </child>
 547                 </widget>
 548                 <packing>
 549                   <property name="tab_expand">False</property>
 550                   <property name="tab_fill">True</property>
 551                 </packing>
 552               </child>
 553
 554               <child>
 555                 <widget class="GtkLabel" id="EasterEggLabel">
 556                   <property name="visible">True</property>
 557                   <property name="label" translatable="yes">WhelpEasterEgg</property>
 558                   <property name="use_underline">False</property>
 559                   <property name="use_markup">False</property>
 560                   <property name="justify">GTK_JUSTIFY_LEFT</property>
 561                   <property name="wrap">False</property>
 562                   <property name="selectable">False</property>
 563                   <property name="xalign">0.5</property>
 564                   <property name="yalign">0.5</property>
 565                   <property name="xpad">0</property>
 566                   <property name="ypad">0</property>
 567                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 568                   <property name="width_chars">-1</property>
 569                   <property name="single_line_mode">False</property>
 570                   <property name="angle">0</property>
 571                 </widget>
 572                 <packing>
 573                   <property name="type">tab</property>
 574                 </packing>
 575               </child>
 576
 577               <child>
 578                 <widget class="GtkScrolledWindow" id="GraphScrolledWin">
 579                   <property name="visible">True</property>
 580                   <property name="can_focus">True</property>
 581                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 582                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
 583                   <property name="shadow_type">GTK_SHADOW_NONE</property>
 584                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 585
 586                   <child>
 587                     <placeholder/>
 588                   </child>
 589                 </widget>
 590                 <packing>
 591                   <property name="tab_expand">False</property>
 592                   <property name="tab_fill">True</property>
 593                 </packing>
 594               </child>
 595
 596               <child>
 597                 <widget class="GtkLabel" id="label26">
 598                   <property name="visible">True</property>
 599                   <property name="label" translatable="yes">Graph</property>
 600                   <property name="use_underline">False</property>
 601                   <property name="use_markup">False</property>
 602                   <property name="justify">GTK_JUSTIFY_LEFT</property>
 603                   <property name="wrap">False</property>
 604                   <property name="selectable">False</property>
 605                   <property name="xalign">0.5</property>
 606                   <property name="yalign">0.5</property>
 607                   <property name="xpad">0</property>
 608                   <property name="ypad">0</property>
 609                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 610                   <property name="width_chars">-1</property>
 611                   <property name="single_line_mode">False</property>
 612                   <property name="angle">0</property>
 613                 </widget>
 614                 <packing>
 615                   <property name="type">tab</property>
 616                 </packing>
 617               </child>
 618             </widget>
 619             <packing>
 620               <property name="padding">0</property>
 621               <property name="expand">True</property>
 622               <property name="fill">True</property>
 623             </packing>
 624           </child>
 625         </widget>
 626       </child>
 627     </widget>
 628   </child>
 629 </widget>
 630
 631 <widget class="GtkDialog" id="ConfirmationDialog">
 632   <property name="title" translatable="yes">DUMMY</property>
 633   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 634   <property name="window_position">GTK_WIN_POS_CENTER</property>
 635   <property name="modal">True</property>
 636   <property name="resizable">False</property>
 637   <property name="destroy_with_parent">False</property>
 638   <property name="decorated">True</property>
 639   <property name="skip_taskbar_hint">False</property>
 640   <property name="skip_pager_hint">False</property>
 641   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 642   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 643   <property name="focus_on_map">True</property>
 644   <property name="urgency_hint">False</property>
 645   <property name="has_separator">True</property>
 646
 647   <child internal-child="vbox">
 648     <widget class="GtkVBox" id="dialog-vbox1">
 649       <property name="visible">True</property>
 650       <property name="homogeneous">False</property>
 651       <property name="spacing">0</property>
 652
 653       <child internal-child="action_area">
 654         <widget class="GtkHButtonBox" id="dialog-action_area1">
 655           <property name="visible">True</property>
 656           <property name="layout_style">GTK_BUTTONBOX_END</property>
 657
 658           <child>
 659             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
 660               <property name="visible">True</property>
 661               <property name="can_default">True</property>
 662               <property name="can_focus">True</property>
 663               <property name="label">gtk-cancel</property>
 664               <property name="use_stock">True</property>
 665               <property name="relief">GTK_RELIEF_NORMAL</property>
 666               <property name="focus_on_click">True</property>
 667               <property name="response_id">-6</property>
 668             </widget>
 669           </child>
 670
 671           <child>
 672             <widget class="GtkButton" id="ConfirmationDialogOkButton">
 673               <property name="visible">True</property>
 674               <property name="can_default">True</property>
 675               <property name="can_focus">True</property>
 676               <property name="label">gtk-ok</property>
 677               <property name="use_stock">True</property>
 678               <property name="relief">GTK_RELIEF_NORMAL</property>
 679               <property name="focus_on_click">True</property>
 680               <property name="response_id">-5</property>
 681             </widget>
 682           </child>
 683         </widget>
 684         <packing>
 685           <property name="padding">0</property>
 686           <property name="expand">False</property>
 687           <property name="fill">True</property>
 688           <property name="pack_type">GTK_PACK_END</property>
 689         </packing>
 690       </child>
 691
 692       <child>
 693         <widget class="GtkLabel" id="ConfirmationDialogLabel">
 694           <property name="visible">True</property>
 695           <property name="label" translatable="yes">DUMMY</property>
 696           <property name="use_underline">False</property>
 697           <property name="use_markup">False</property>
 698           <property name="justify">GTK_JUSTIFY_CENTER</property>
 699           <property name="wrap">False</property>
 700           <property name="selectable">False</property>
 701           <property name="xalign">0.5</property>
 702           <property name="yalign">0.5</property>
 703           <property name="xpad">0</property>
 704           <property name="ypad">0</property>
 705           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 706           <property name="width_chars">-1</property>
 707           <property name="single_line_mode">False</property>
 708           <property name="angle">0</property>
 709         </widget>
 710         <packing>
 711           <property name="padding">0</property>
 712           <property name="expand">False</property>
 713           <property name="fill">False</property>
 714         </packing>
 715       </child>
 716     </widget>
 717   </child>
 718 </widget>
 719
 720 <widget class="GtkDialog" id="EmptyDialog">
 721   <property name="visible">True</property>
 722   <property name="title" translatable="yes">DUMMY</property>
 723   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 724   <property name="window_position">GTK_WIN_POS_NONE</property>
 725   <property name="modal">False</property>
 726   <property name="resizable">True</property>
 727   <property name="destroy_with_parent">False</property>
 728   <property name="decorated">True</property>
 729   <property name="skip_taskbar_hint">False</property>
 730   <property name="skip_pager_hint">False</property>
 731   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 732   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 733   <property name="focus_on_map">True</property>
 734   <property name="urgency_hint">False</property>
 735   <property name="has_separator">True</property>
 736
 737   <child internal-child="vbox">
 738     <widget class="GtkVBox" id="EmptyDialogVBox">
 739       <property name="visible">True</property>
 740       <property name="homogeneous">False</property>
 741       <property name="spacing">0</property>
 742
 743       <child internal-child="action_area">
 744         <widget class="GtkHButtonBox" id="dialog-action_area5">
 745           <property name="visible">True</property>
 746           <property name="layout_style">GTK_BUTTONBOX_END</property>
 747
 748           <child>
 749             <widget class="GtkButton" id="EmptyDialogCancelButton">
 750               <property name="visible">True</property>
 751               <property name="can_default">True</property>
 752               <property name="can_focus">True</property>
 753               <property name="label">gtk-cancel</property>
 754               <property name="use_stock">True</property>
 755               <property name="relief">GTK_RELIEF_NORMAL</property>
 756               <property name="focus_on_click">True</property>
 757               <property name="response_id">-6</property>
 758             </widget>
 759           </child>
 760
 761           <child>
 762             <widget class="GtkButton" id="EmptyDialogOkButton">
 763               <property name="visible">True</property>
 764               <property name="can_default">True</property>
 765               <property name="can_focus">True</property>
 766               <property name="label">gtk-ok</property>
 767               <property name="use_stock">True</property>
 768               <property name="relief">GTK_RELIEF_NORMAL</property>
 769               <property name="focus_on_click">True</property>
 770               <property name="response_id">-5</property>
 771             </widget>
 772           </child>
 773         </widget>
 774         <packing>
 775           <property name="padding">0</property>
 776           <property name="expand">False</property>
 777           <property name="fill">True</property>
 778           <property name="pack_type">GTK_PACK_END</property>
 779         </packing>
 780       </child>
 781
 782       <child>
 783         <widget class="GtkLabel" id="EmptyDialogLabel">
 784           <property name="visible">True</property>
 785           <property name="label" translatable="yes">DUMMY</property>
 786           <property name="use_underline">False</property>
 787           <property name="use_markup">False</property>
 788           <property name="justify">GTK_JUSTIFY_LEFT</property>
 789           <property name="wrap">False</property>
 790           <property name="selectable">False</property>
 791           <property name="xalign">0.5</property>
 792           <property name="yalign">0.5</property>
 793           <property name="xpad">0</property>
 794           <property name="ypad">0</property>
 795           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
 796           <property name="width_chars">-1</property>
 797           <property name="single_line_mode">False</property>
 798           <property name="angle">0</property>
 799         </widget>
 800         <packing>
 801           <property name="padding">0</property>
 802           <property name="expand">False</property>
 803           <property name="fill">False</property>
 804         </packing>
 805       </child>
 806
 807       <child>
 808         <placeholder/>
 809       </child>
 810     </widget>
 811   </child>
 812 </widget>
 813
 814 <widget class="GtkFileSelection" id="FileSelectionWin">
 815   <property name="border_width">10</property>
 816   <property name="title" translatable="yes">Select File</property>
 817   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 818   <property name="window_position">GTK_WIN_POS_CENTER</property>
 819   <property name="modal">True</property>
 820   <property name="resizable">True</property>
 821   <property name="destroy_with_parent">False</property>
 822   <property name="decorated">True</property>
 823   <property name="skip_taskbar_hint">False</property>
 824   <property name="skip_pager_hint">False</property>
 825   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
 826   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 827   <property name="focus_on_map">True</property>
 828   <property name="urgency_hint">False</property>
 829   <property name="show_fileops">True</property>
 830
 831   <child internal-child="cancel_button">
 832     <widget class="GtkButton" id="fileSelCancelButton">
 833       <property name="visible">True</property>
 834       <property name="can_default">True</property>
 835       <property name="can_focus">True</property>
 836       <property name="relief">GTK_RELIEF_NORMAL</property>
 837       <property name="focus_on_click">True</property>
 838     </widget>
 839   </child>
 840
 841   <child internal-child="ok_button">
 842     <widget class="GtkButton" id="fileSelOkButton">
 843       <property name="visible">True</property>
 844       <property name="can_default">True</property>
 845       <property name="can_focus">True</property>
 846       <property name="relief">GTK_RELIEF_NORMAL</property>
 847       <property name="focus_on_click">True</property>
 848     </widget>
 849   </child>
 850 </widget>
 851
 852 <widget class="GtkWindow" id="MainWin">
 853   <property name="title" translatable="yes">Matita</property>
 854   <property name="type">GTK_WINDOW_TOPLEVEL</property>
 855   <property name="window_position">GTK_WIN_POS_NONE</property>
 856   <property name="modal">False</property>
 857   <property name="resizable">True</property>
 858   <property name="destroy_with_parent">False</property>
 859   <property name="decorated">True</property>
 860   <property name="skip_taskbar_hint">False</property>
 861   <property name="skip_pager_hint">False</property>
 862   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
 863   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
 864   <property name="focus_on_map">True</property>
 865   <property name="urgency_hint">False</property>
 866
 867   <child>
 868     <widget class="GtkEventBox" id="MainWinEventBox">
 869       <property name="visible">True</property>
 870       <property name="visible_window">True</property>
 871       <property name="above_child">False</property>
 872
 873       <child>
 874         <widget class="GtkVBox" id="vbox8">
 875           <property name="visible">True</property>
 876           <property name="homogeneous">False</property>
 877           <property name="spacing">0</property>
 878
 879           <child>
 880             <widget class="GtkHandleBox" id="menuBarHandleBox">
 881               <property name="visible">True</property>
 882               <property name="shadow_type">GTK_SHADOW_OUT</property>
 883               <property name="handle_position">GTK_POS_LEFT</property>
 884               <property name="snap_edge">GTK_POS_TOP</property>
 885
 886               <child>
 887                 <widget class="GtkMenuBar" id="menubar1">
 888                   <property name="visible">True</property>
 889                   <property name="pack_direction">GTK_PACK_DIRECTION_LTR</property>
 890                   <property name="child_pack_direction">GTK_PACK_DIRECTION_LTR</property>
 891
 892                   <child>
 893                     <widget class="GtkMenuItem" id="fileMenu">
 894                       <property name="visible">True</property>
 895                       <property name="label" translatable="yes">_File</property>
 896                       <property name="use_underline">True</property>
 897
 898                       <child>
 899                         <widget class="GtkMenu" id="fileMenu_menu">
 900
 901                           <child>
 902                             <widget class="GtkImageMenuItem" id="newMenuItem">
 903                               <property name="visible">True</property>
 904                               <property name="label" translatable="yes">_New</property>
 905                               <property name="use_underline">True</property>
 906                               <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 907
 908                               <child internal-child="image">
 909                                 <widget class="GtkImage" id="image889">
 910                                   <property name="visible">True</property>
 911                                   <property name="stock">gtk-new</property>
 912                                   <property name="icon_size">1</property>
 913                                   <property name="xalign">0.5</property>
 914                                   <property name="yalign">0.5</property>
 915                                   <property name="xpad">0</property>
 916                                   <property name="ypad">0</property>
 917                                 </widget>
 918                               </child>
 919                             </widget>
 920                           </child>
 921
 922                           <child>
 923                             <widget class="GtkImageMenuItem" id="openMenuItem">
 924                               <property name="visible">True</property>
 925                               <property name="label" translatable="yes">_Open...</property>
 926                               <property name="use_underline">True</property>
 927                               <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 928
 929                               <child internal-child="image">
 930                                 <widget class="GtkImage" id="image890">
 931                                   <property name="visible">True</property>
 932                                   <property name="stock">gtk-open</property>
 933                                   <property name="icon_size">1</property>
 934                                   <property name="xalign">0.5</property>
 935                                   <property name="yalign">0.5</property>
 936                                   <property name="xpad">0</property>
 937                                   <property name="ypad">0</property>
 938                                 </widget>
 939                               </child>
 940                             </widget>
 941                           </child>
 942
 943                           <child>
 944                             <widget class="GtkImageMenuItem" id="saveMenuItem">
 945                               <property name="visible">True</property>
 946                               <property name="label" translatable="yes">_Save</property>
 947                               <property name="use_underline">True</property>
 948                               <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 949
 950                               <child internal-child="image">
 951                                 <widget class="GtkImage" id="image891">
 952                                   <property name="visible">True</property>
 953                                   <property name="stock">gtk-save</property>
 954                                   <property name="icon_size">1</property>
 955                                   <property name="xalign">0.5</property>
 956                                   <property name="yalign">0.5</property>
 957                                   <property name="xpad">0</property>
 958                                   <property name="ypad">0</property>
 959                                 </widget>
 960                               </child>
 961                             </widget>
 962                           </child>
 963
 964                           <child>
 965                             <widget class="GtkImageMenuItem" id="saveAsMenuItem">
 966                               <property name="visible">True</property>
 967                               <property name="label" translatable="yes">Save _As ...</property>
 968                               <property name="use_underline">True</property>
 969                               <accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 970
 971                               <child internal-child="image">
 972                                 <widget class="GtkImage" id="image892">
 973                                   <property name="visible">True</property>
 974                                   <property name="stock">gtk-save-as</property>
 975                                   <property name="icon_size">1</property>
 976                                   <property name="xalign">0.5</property>
 977                                   <property name="yalign">0.5</property>
 978                                   <property name="xpad">0</property>
 979                                   <property name="ypad">0</property>
 980                                 </widget>
 981                               </child>
 982                             </widget>
 983                           </child>
 984
 985                           <child>
 986                             <widget class="GtkImageMenuItem" id="developmentsMenuItem">
 987                               <property name="visible">True</property>
 988                               <property name="label" translatable="yes">_Developments...</property>
 989                               <property name="use_underline">True</property>
 990                               <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 991
 992                               <child internal-child="image">
 993                                 <widget class="GtkImage" id="image893">
 994                                   <property name="visible">True</property>
 995                                   <property name="stock">gtk-execute</property>
 996                                   <property name="icon_size">1</property>
 997                                   <property name="xalign">0.5</property>
 998                                   <property name="yalign">0.5</property>
 999                                   <property name="xpad">0</property>
1000                                   <property name="ypad">0</property>
1001                                 </widget>
1002                               </child>
1003                             </widget>
1004                           </child>
1005
1006                           <child>
1007                             <widget class="GtkSeparatorMenuItem" id="separator2">
1008                               <property name="visible">True</property>
1009                             </widget>
1010                           </child>
1011
1012                           <child>
1013                             <widget class="GtkImageMenuItem" id="quitMenuItem">
1014                               <property name="visible">True</property>
1015                               <property name="label" translatable="yes">_Quit</property>
1016                               <property name="use_underline">True</property>
1017                               <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1018
1019                               <child internal-child="image">
1020                                 <widget class="GtkImage" id="image894">
1021                                   <property name="visible">True</property>
1022                                   <property name="stock">gtk-quit</property>
1023                                   <property name="icon_size">1</property>
1024                                   <property name="xalign">0.5</property>
1025                                   <property name="yalign">0.5</property>
1026                                   <property name="xpad">0</property>
1027                                   <property name="ypad">0</property>
1028                                 </widget>
1029                               </child>
1030                             </widget>
1031                           </child>
1032                         </widget>
1033                       </child>
1034                     </widget>
1035                   </child>
1036
1037                   <child>
1038                     <widget class="GtkMenuItem" id="editMenu">
1039                       <property name="visible">True</property>
1040                       <property name="label" translatable="yes">_Edit</property>
1041                       <property name="use_underline">True</property>
1042
1043                       <child>
1044                         <widget class="GtkMenu" id="editMenu_menu">
1045
1046                           <child>
1047                             <widget class="GtkImageMenuItem" id="undoMenuItem">
1048                               <property name="visible">True</property>
1049                               <property name="sensitive">False</property>
1050                               <property name="label" translatable="yes">_Undo</property>
1051                               <property name="use_underline">True</property>
1052                               <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1053
1054                               <child internal-child="image">
1055                                 <widget class="GtkImage" id="image895">
1056                                   <property name="visible">True</property>
1057                                   <property name="stock">gtk-undo</property>
1058                                   <property name="icon_size">1</property>
1059                                   <property name="xalign">0.5</property>
1060                                   <property name="yalign">0.5</property>
1061                                   <property name="xpad">0</property>
1062                                   <property name="ypad">0</property>
1063                                 </widget>
1064                               </child>
1065                             </widget>
1066                           </child>
1067
1068                           <child>
1069                             <widget class="GtkImageMenuItem" id="redoMenuItem">
1070                               <property name="visible">True</property>
1071                               <property name="sensitive">False</property>
1072                               <property name="label" translatable="yes">_Redo</property>
1073                               <property name="use_underline">True</property>
1074                               <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
1075
1076                               <child internal-child="image">
1077                                 <widget class="GtkImage" id="image896">
1078                                   <property name="visible">True</property>
1079                                   <property name="stock">gtk-redo</property>
1080                                   <property name="icon_size">1</property>
1081                                   <property name="xalign">0.5</property>
1082                                   <property name="yalign">0.5</property>
1083                                   <property name="xpad">0</property>
1084                                   <property name="ypad">0</property>
1085                                 </widget>
1086                               </child>
1087                             </widget>
1088                           </child>
1089
1090                           <child>
1091                             <widget class="GtkSeparatorMenuItem" id="separator3">
1092                               <property name="visible">True</property>
1093                             </widget>
1094                           </child>
1095
1096                           <child>
1097                             <widget class="GtkImageMenuItem" id="cutMenuItem">
1098                               <property name="visible">True</property>
1099                               <property name="label" translatable="yes">Cu_t</property>
1100                               <property name="use_underline">True</property>
1101                               <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1102
1103                               <child internal-child="image">
1104                                 <widget class="GtkImage" id="image897">
1105                                   <property name="visible">True</property>
1106                                   <property name="stock">gtk-cut</property>
1107                                   <property name="icon_size">1</property>
1108                                   <property name="xalign">0.5</property>
1109                                   <property name="yalign">0.5</property>
1110                                   <property name="xpad">0</property>
1111                                   <property name="ypad">0</property>
1112                                 </widget>
1113                               </child>
1114                             </widget>
1115                           </child>
1116
1117                           <child>
1118                             <widget class="GtkImageMenuItem" id="copyMenuItem">
1119                               <property name="visible">True</property>
1120                               <property name="label" translatable="yes">_Copy</property>
1121                               <property name="use_underline">True</property>
1122                               <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1123
1124                               <child internal-child="image">
1125                                 <widget class="GtkImage" id="image898">
1126                                   <property name="visible">True</property>
1127                                   <property name="stock">gtk-copy</property>
1128                                   <property name="icon_size">1</property>
1129                                   <property name="xalign">0.5</property>
1130                                   <property name="yalign">0.5</property>
1131                                   <property name="xpad">0</property>
1132                                   <property name="ypad">0</property>
1133                                 </widget>
1134                               </child>
1135                             </widget>
1136                           </child>
1137
1138                           <child>
1139                             <widget class="GtkImageMenuItem" id="pasteMenuItem">
1140                               <property name="visible">True</property>
1141                               <property name="label" translatable="yes">_Paste</property>
1142                               <property name="use_underline">True</property>
1143                               <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1144
1145                               <child internal-child="image">
1146                                 <widget class="GtkImage" id="image899">
1147                                   <property name="visible">True</property>
1148                                   <property name="stock">gtk-paste</property>
1149                                   <property name="icon_size">1</property>
1150                                   <property name="xalign">0.5</property>
1151                                   <property name="yalign">0.5</property>
1152                                   <property name="xpad">0</property>
1153                                   <property name="ypad">0</property>
1154                                 </widget>
1155                               </child>
1156                             </widget>
1157                           </child>
1158
1159                           <child>
1160                             <widget class="GtkMenuItem" id="pastePatternMenuItem">
1161                               <property name="visible">True</property>
1162                               <property name="label" translatable="yes">Paste as pattern</property>
1163                               <property name="use_underline">True</property>
1164                             </widget>
1165                           </child>
1166
1167                           <child>
1168                             <widget class="GtkImageMenuItem" id="deleteMenuItem">
1169                               <property name="visible">True</property>
1170                               <property name="label" translatable="yes">_Delete</property>
1171                               <property name="use_underline">True</property>
1172
1173                               <child internal-child="image">
1174                                 <widget class="GtkImage" id="image900">
1175                                   <property name="visible">True</property>
1176                                   <property name="stock">gtk-delete</property>
1177                                   <property name="icon_size">1</property>
1178                                   <property name="xalign">0.5</property>
1179                                   <property name="yalign">0.5</property>
1180                                   <property name="xpad">0</property>
1181                                   <property name="ypad">0</property>
1182                                 </widget>
1183                               </child>
1184                             </widget>
1185                           </child>
1186
1187                           <child>
1188                             <widget class="GtkSeparatorMenuItem" id="separator4">
1189                               <property name="visible">True</property>
1190                             </widget>
1191                           </child>
1192
1193                           <child>
1194                             <widget class="GtkMenuItem" id="selectAllMenuItem">
1195                               <property name="visible">True</property>
1196                               <property name="label" translatable="yes">Select _All</property>
1197                               <property name="use_underline">True</property>
1198                             </widget>
1199                           </child>
1200
1201                           <child>
1202                             <widget class="GtkSeparatorMenuItem" id="separator7">
1203                               <property name="visible">True</property>
1204                             </widget>
1205                           </child>
1206
1207                           <child>
1208                             <widget class="GtkImageMenuItem" id="findReplMenuItem">
1209                               <property name="visible">True</property>
1210                               <property name="label" translatable="yes">_Find &amp; Replace ...</property>
1211                               <property name="use_underline">True</property>
1212                               <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1213
1214                               <child internal-child="image">
1215                                 <widget class="GtkImage" id="image901">
1216                                   <property name="visible">True</property>
1217                                   <property name="stock">gtk-find-and-replace</property>
1218                                   <property name="icon_size">1</property>
1219                                   <property name="xalign">0.5</property>
1220                                   <property name="yalign">0.5</property>
1221                                   <property name="xpad">0</property>
1222                                   <property name="ypad">0</property>
1223                                 </widget>
1224                               </child>
1225                             </widget>
1226                           </child>
1227
1228                           <child>
1229                             <widget class="GtkSeparatorMenuItem" id="separator8">
1230                               <property name="visible">True</property>
1231                             </widget>
1232                           </child>
1233
1234                           <child>
1235                             <widget class="GtkMenuItem" id="LigatureButton">
1236                               <property name="visible">True</property>
1237                               <property name="label" translatable="yes">Next ligature</property>
1238                               <property name="use_underline">True</property>
1239                               <accelerator key="l" modifiers="GDK_MOD1_MASK" signal="activate"/>
1240                             </widget>
1241                           </child>
1242
1243                           <child>
1244                             <widget class="GtkMenuItem" id="externalEditorMenuItem">
1245                               <property name="visible">True</property>
1246                               <property name="label" translatable="yes">Edit with E_xternal Editor</property>
1247                               <property name="use_underline">True</property>
1248                             </widget>
1249                           </child>
1250                         </widget>
1251                       </child>
1252                     </widget>
1253                   </child>
1254
1255                   <child>
1256                     <widget class="GtkMenuItem" id="scriptMenu">
1257                       <property name="visible">True</property>
1258                       <property name="label" translatable="yes">_Script</property>
1259                       <property name="use_underline">True</property>
1260
1261                       <child>
1262                         <widget class="GtkMenu" id="scriptMenu_menu">
1263
1264                           <child>
1265                             <widget class="GtkMenuItem" id="scriptAdvanceMenuItem">
1266                               <property name="visible">True</property>
1267                               <property name="label" translatable="yes">Execute 1 phrase</property>
1268                               <property name="use_underline">True</property>
1269                               <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1270                             </widget>
1271                           </child>
1272
1273                           <child>
1274                             <widget class="GtkMenuItem" id="scriptRetractMenuItem">
1275                               <property name="visible">True</property>
1276                               <property name="label" translatable="yes">Retract 1 phrase</property>
1277                               <property name="use_underline">True</property>
1278                               <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1279                             </widget>
1280                           </child>
1281
1282                           <child>
1283                             <widget class="GtkSeparatorMenuItem" id="separator9">
1284                               <property name="visible">True</property>
1285                             </widget>
1286                           </child>
1287
1288                           <child>
1289                             <widget class="GtkMenuItem" id="scriptBottomMenuItem">
1290                               <property name="visible">True</property>
1291                               <property name="label" translatable="yes">Execute all</property>
1292                               <property name="use_underline">True</property>
1293                               <accelerator key="End" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1294                             </widget>
1295                           </child>
1296
1297                           <child>
1298                             <widget class="GtkMenuItem" id="scriptTopMenuItem">
1299                               <property name="visible">True</property>
1300                               <property name="label" translatable="yes">Restart</property>
1301                               <property name="use_underline">True</property>
1302                               <accelerator key="Home" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1303                             </widget>
1304                           </child>
1305
1306                           <child>
1307                             <widget class="GtkSeparatorMenuItem" id="separator10">
1308                               <property name="visible">True</property>
1309                             </widget>
1310                           </child>
1311
1312                           <child>
1313                             <widget class="GtkMenuItem" id="scriptJumpMenuItem">
1314                               <property name="visible">True</property>
1315                               <property name="label" translatable="yes">Execute until cursor</property>
1316                               <property name="use_underline">True</property>
1317                               <accelerator key="period" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK" signal="activate"/>
1318                             </widget>
1319                           </child>
1320                         </widget>
1321                       </child>
1322                     </widget>
1323                   </child>
1324
1325                   <child>
1326                     <widget class="GtkMenuItem" id="viewMenu">
1327                       <property name="visible">True</property>
1328                       <property name="label" translatable="yes">_View</property>
1329                       <property name="use_underline">True</property>
1330
1331                       <child>
1332                         <widget class="GtkMenu" id="viewMenu_menu">
1333
1334                           <child>
1335                             <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
1336                               <property name="visible">True</property>
1337                               <property name="label" translatable="yes">Show _Tactics Bar</property>
1338                               <property name="use_underline">True</property>
1339                               <property name="active">True</property>
1340                               <accelerator key="F2" modifiers="0" signal="activate"/>
1341                             </widget>
1342                           </child>
1343
1344                           <child>
1345                             <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1346                               <property name="visible">True</property>
1347                               <property name="label" translatable="yes">New Cic _Browser</property>
1348                               <property name="use_underline">True</property>
1349                               <accelerator key="F3" modifiers="0" signal="activate"/>
1350                             </widget>
1351                           </child>
1352
1353                           <child>
1354                             <widget class="GtkSeparatorMenuItem" id="separator5">
1355                               <property name="visible">True</property>
1356                             </widget>
1357                           </child>
1358
1359                           <child>
1360                             <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1361                               <property name="visible">True</property>
1362                               <property name="label" translatable="yes">_Fullscreen</property>
1363                               <property name="use_underline">True</property>
1364                               <property name="active">False</property>
1365                               <accelerator key="F11" modifiers="0" signal="activate"/>
1366                             </widget>
1367                           </child>
1368
1369                           <child>
1370                             <widget class="GtkSeparatorMenuItem" id="separator1">
1371                               <property name="visible">True</property>
1372                             </widget>
1373                           </child>
1374
1375                           <child>
1376                             <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
1377                               <property name="visible">True</property>
1378                               <property name="label" translatable="yes">Zoom _In</property>
1379                               <property name="use_underline">True</property>
1380                               <signal name="activate" handler="on_increaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1381                               <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1382
1383                               <child internal-child="image">
1384                                 <widget class="GtkImage" id="image902">
1385                                   <property name="visible">True</property>
1386                                   <property name="stock">gtk-zoom-in</property>
1387                                   <property name="icon_size">1</property>
1388                                   <property name="xalign">0.5</property>
1389                                   <property name="yalign">0.5</property>
1390                                   <property name="xpad">0</property>
1391                                   <property name="ypad">0</property>
1392                                 </widget>
1393                               </child>
1394                             </widget>
1395                           </child>
1396
1397                           <child>
1398                             <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
1399                               <property name="visible">True</property>
1400                               <property name="label" translatable="yes">Zoom _Out</property>
1401                               <property name="use_underline">True</property>
1402                               <signal name="activate" handler="on_decreaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1403                               <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1404
1405                               <child internal-child="image">
1406                                 <widget class="GtkImage" id="image903">
1407                                   <property name="visible">True</property>
1408                                   <property name="stock">gtk-zoom-out</property>
1409                                   <property name="icon_size">1</property>
1410                                   <property name="xalign">0.5</property>
1411                                   <property name="yalign">0.5</property>
1412                                   <property name="xpad">0</property>
1413                                   <property name="ypad">0</property>
1414                                 </widget>
1415                               </child>
1416                             </widget>
1417                           </child>
1418
1419                           <child>
1420                             <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
1421                               <property name="visible">True</property>
1422                               <property name="label" translatable="yes">_Normal Size</property>
1423                               <property name="use_underline">True</property>
1424                               <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1425
1426                               <child internal-child="image">
1427                                 <widget class="GtkImage" id="image904">
1428                                   <property name="visible">True</property>
1429                                   <property name="stock">gtk-zoom-100</property>
1430                                   <property name="icon_size">1</property>
1431                                   <property name="xalign">0.5</property>
1432                                   <property name="yalign">0.5</property>
1433                                   <property name="xpad">0</property>
1434                                   <property name="ypad">0</property>
1435                                 </widget>
1436                               </child>
1437                             </widget>
1438                           </child>
1439                         </widget>
1440                       </child>
1441                     </widget>
1442                   </child>
1443
1444                   <child>
1445                     <widget class="GtkMenuItem" id="debugMenu">
1446                       <property name="visible">True</property>
1447                       <property name="label" translatable="yes">_Debug</property>
1448                       <property name="use_underline">True</property>
1449
1450                       <child>
1451                         <widget class="GtkMenu" id="debugMenu_menu">
1452
1453                           <child>
1454                             <widget class="GtkSeparatorMenuItem" id="separator6">
1455                               <property name="visible">True</property>
1456                             </widget>
1457                           </child>
1458                         </widget>
1459                       </child>
1460                     </widget>
1461                   </child>
1462
1463                   <child>
1464                     <widget class="GtkMenuItem" id="helpMenu">
1465                       <property name="visible">True</property>
1466                       <property name="label" translatable="yes">_Help</property>
1467                       <property name="use_underline">True</property>
1468
1469                       <child>
1470                         <widget class="GtkMenu" id="helpMenu_menu">
1471
1472                           <child>
1473                             <widget class="GtkImageMenuItem" id="contentsMenuItem">
1474                               <property name="visible">True</property>
1475                               <property name="label" translatable="yes">_Contents</property>
1476                               <property name="use_underline">True</property>
1477                               <accelerator key="F1" modifiers="0" signal="activate"/>
1478
1479                               <child internal-child="image">
1480                                 <widget class="GtkImage" id="image905">
1481                                   <property name="visible">True</property>
1482                                   <property name="stock">gtk-help</property>
1483                                   <property name="icon_size">1</property>
1484                                   <property name="xalign">0.5</property>
1485                                   <property name="yalign">0.5</property>
1486                                   <property name="xpad">0</property>
1487                                   <property name="ypad">0</property>
1488                                 </widget>
1489                               </child>
1490                             </widget>
1491                           </child>
1492
1493                           <child>
1494                             <widget class="GtkImageMenuItem" id="aboutMenuItem">
1495                               <property name="visible">True</property>
1496                               <property name="label" translatable="yes">_About</property>
1497                               <property name="use_underline">True</property>
1498
1499                               <child internal-child="image">
1500                                 <widget class="GtkImage" id="image906">
1501                                   <property name="visible">True</property>
1502                                   <property name="stock">gtk-about</property>
1503                                   <property name="icon_size">1</property>
1504                                   <property name="xalign">0.5</property>
1505                                   <property name="yalign">0.5</property>
1506                                   <property name="xpad">0</property>
1507                                   <property name="ypad">0</property>
1508                                 </widget>
1509                               </child>
1510                             </widget>
1511                           </child>
1512                         </widget>
1513                       </child>
1514                     </widget>
1515                   </child>
1516                 </widget>
1517               </child>
1518             </widget>
1519             <packing>
1520               <property name="padding">0</property>
1521               <property name="expand">False</property>
1522               <property name="fill">False</property>
1523             </packing>
1524           </child>
1525
1526           <child>
1527             <widget class="GtkHBox" id="hbox9">
1528               <property name="visible">True</property>
1529               <property name="homogeneous">False</property>
1530               <property name="spacing">0</property>
1531
1532               <child>
1533                 <widget class="GtkHPaned" id="hpaneScriptSequent">
1534                   <property name="visible">True</property>
1535                   <property name="can_focus">True</property>
1536
1537                   <child>
1538                     <widget class="GtkHBox" id="hbox18">
1539                       <property name="visible">True</property>
1540                       <property name="homogeneous">False</property>
1541                       <property name="spacing">0</property>
1542
1543                       <child>
1544                         <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1545                           <property name="visible">True</property>
1546                           <property name="shadow_type">GTK_SHADOW_OUT</property>
1547                           <property name="handle_position">GTK_POS_TOP</property>
1548                           <property name="snap_edge">GTK_POS_TOP</property>
1549
1550                           <child>
1551                             <widget class="GtkTable" id="ToolBarTable">
1552                               <property name="visible">True</property>
1553                               <property name="n_rows">17</property>
1554                               <property name="n_columns">2</property>
1555                               <property name="homogeneous">False</property>
1556                               <property name="row_spacing">4</property>
1557                               <property name="column_spacing">0</property>
1558
1559                               <child>
1560                                 <widget class="GtkButton" id="applyButton">
1561                                   <property name="visible">True</property>
1562                                   <property name="tooltip" translatable="yes">Apply</property>
1563                                   <property name="can_focus">True</property>
1564                                   <property name="label" translatable="yes">apply</property>
1565                                   <property name="use_underline">True</property>
1566                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1567                                   <property name="focus_on_click">True</property>
1568                                 </widget>
1569                                 <packing>
1570                                   <property name="left_attach">1</property>
1571                                   <property name="right_attach">2</property>
1572                                   <property name="top_attach">0</property>
1573                                   <property name="bottom_attach">1</property>
1574                                   <property name="x_options">fill</property>
1575                                   <property name="y_options"></property>
1576                                 </packing>
1577                               </child>
1578
1579                               <child>
1580                                 <widget class="GtkButton" id="introsButton">
1581                                   <property name="visible">True</property>
1582                                   <property name="tooltip" translatable="yes">Intros</property>
1583                                   <property name="can_focus">True</property>
1584                                   <property name="label" translatable="yes">intro</property>
1585                                   <property name="use_underline">True</property>
1586                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1587                                   <property name="focus_on_click">True</property>
1588                                 </widget>
1589                                 <packing>
1590                                   <property name="left_attach">0</property>
1591                                   <property name="right_attach">1</property>
1592                                   <property name="top_attach">0</property>
1593                                   <property name="bottom_attach">1</property>
1594                                   <property name="x_options">fill</property>
1595                                   <property name="y_options"></property>
1596                                 </packing>
1597                               </child>
1598
1599                               <child>
1600                                 <widget class="GtkButton" id="exactButton">
1601                                   <property name="visible">True</property>
1602                                   <property name="tooltip" translatable="yes">Exact</property>
1603                                   <property name="can_focus">True</property>
1604                                   <property name="label" translatable="yes">exact</property>
1605                                   <property name="use_underline">True</property>
1606                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1607                                   <property name="focus_on_click">True</property>
1608                                 </widget>
1609                                 <packing>
1610                                   <property name="left_attach">0</property>
1611                                   <property name="right_attach">1</property>
1612                                   <property name="top_attach">2</property>
1613                                   <property name="bottom_attach">3</property>
1614                                   <property name="x_options">fill</property>
1615                                   <property name="y_options"></property>
1616                                 </packing>
1617                               </child>
1618
1619                               <child>
1620                                 <widget class="GtkButton" id="elimButton">
1621                                   <property name="visible">True</property>
1622                                   <property name="tooltip" translatable="yes">Elim</property>
1623                                   <property name="can_focus">True</property>
1624                                   <property name="label" translatable="yes">elim</property>
1625                                   <property name="use_underline">True</property>
1626                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1627                                   <property name="focus_on_click">True</property>
1628                                 </widget>
1629                                 <packing>
1630                                   <property name="left_attach">0</property>
1631                                   <property name="right_attach">1</property>
1632                                   <property name="top_attach">4</property>
1633                                   <property name="bottom_attach">5</property>
1634                                   <property name="x_options">fill</property>
1635                                   <property name="y_options"></property>
1636                                 </packing>
1637                               </child>
1638
1639                               <child>
1640                                 <widget class="GtkButton" id="reflexivityButton">
1641                                   <property name="visible">True</property>
1642                                   <property name="tooltip" translatable="yes">Reflexivity</property>
1643                                   <property name="can_focus">True</property>
1644                                   <property name="label" translatable="yes">refl</property>
1645                                   <property name="use_underline">True</property>
1646                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1647                                   <property name="focus_on_click">True</property>
1648                                 </widget>
1649                                 <packing>
1650                                   <property name="left_attach">0</property>
1651                                   <property name="right_attach">1</property>
1652                                   <property name="top_attach">8</property>
1653                                   <property name="bottom_attach">9</property>
1654                                   <property name="x_options">fill</property>
1655                                   <property name="y_options"></property>
1656                                 </packing>
1657                               </child>
1658
1659                               <child>
1660                                 <widget class="GtkButton" id="symmetryButton">
1661                                   <property name="visible">True</property>
1662                                   <property name="tooltip" translatable="yes">Symmetry</property>
1663                                   <property name="can_focus">True</property>
1664                                   <property name="label" translatable="yes">sym</property>
1665                                   <property name="use_underline">True</property>
1666                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1667                                   <property name="focus_on_click">True</property>
1668                                 </widget>
1669                                 <packing>
1670                                   <property name="left_attach">1</property>
1671                                   <property name="right_attach">2</property>
1672                                   <property name="top_attach">8</property>
1673                                   <property name="bottom_attach">9</property>
1674                                   <property name="x_options">fill</property>
1675                                   <property name="y_options"></property>
1676                                 </packing>
1677                               </child>
1678
1679                               <child>
1680                                 <widget class="GtkButton" id="transitivityButton">
1681                                   <property name="visible">True</property>
1682                                   <property name="tooltip" translatable="yes">Transitivity</property>
1683                                   <property name="can_focus">True</property>
1684                                   <property name="label" translatable="yes">trans</property>
1685                                   <property name="use_underline">True</property>
1686                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1687                                   <property name="focus_on_click">True</property>
1688                                 </widget>
1689                                 <packing>
1690                                   <property name="left_attach">0</property>
1691                                   <property name="right_attach">1</property>
1692                                   <property name="top_attach">9</property>
1693                                   <property name="bottom_attach">10</property>
1694                                   <property name="x_options">fill</property>
1695                                   <property name="y_options"></property>
1696                                 </packing>
1697                               </child>
1698
1699                               <child>
1700                                 <widget class="GtkButton" id="simplifyButton">
1701                                   <property name="visible">True</property>
1702                                   <property name="tooltip" translatable="yes">Simplify</property>
1703                                   <property name="can_focus">True</property>
1704                                   <property name="label" translatable="yes">simpl</property>
1705                                   <property name="use_underline">True</property>
1706                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1707                                   <property name="focus_on_click">True</property>
1708                                 </widget>
1709                                 <packing>
1710                                   <property name="left_attach">0</property>
1711                                   <property name="right_attach">1</property>
1712                                   <property name="top_attach">11</property>
1713                                   <property name="bottom_attach">12</property>
1714                                   <property name="x_options">fill</property>
1715                                   <property name="y_options"></property>
1716                                 </packing>
1717                               </child>
1718
1719                               <child>
1720                                 <widget class="GtkButton" id="reduceButton">
1721                                   <property name="visible">True</property>
1722                                   <property name="tooltip" translatable="yes">Reduce</property>
1723                                   <property name="can_focus">True</property>
1724                                   <property name="label" translatable="yes">red</property>
1725                                   <property name="use_underline">True</property>
1726                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1727                                   <property name="focus_on_click">True</property>
1728                                 </widget>
1729                                 <packing>
1730                                   <property name="left_attach">1</property>
1731                                   <property name="right_attach">2</property>
1732                                   <property name="top_attach">11</property>
1733                                   <property name="bottom_attach">12</property>
1734                                   <property name="x_options">fill</property>
1735                                   <property name="y_options"></property>
1736                                 </packing>
1737                               </child>
1738
1739                               <child>
1740                                 <widget class="GtkButton" id="whdButton">
1741                                   <property name="visible">True</property>
1742                                   <property name="tooltip" translatable="yes">Whd</property>
1743                                   <property name="can_focus">True</property>
1744                                   <property name="label" translatable="yes">whd</property>
1745                                   <property name="use_underline">True</property>
1746                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1747                                   <property name="focus_on_click">True</property>
1748                                 </widget>
1749                                 <packing>
1750                                   <property name="left_attach">0</property>
1751                                   <property name="right_attach">1</property>
1752                                   <property name="top_attach">12</property>
1753                                   <property name="bottom_attach">13</property>
1754                                   <property name="x_options">fill</property>
1755                                   <property name="y_options"></property>
1756                                 </packing>
1757                               </child>
1758
1759                               <child>
1760                                 <widget class="GtkButton" id="assumptionButton">
1761                                   <property name="visible">True</property>
1762                                   <property name="tooltip" translatable="yes">Assumption</property>
1763                                   <property name="can_focus">True</property>
1764                                   <property name="label" translatable="yes">assum</property>
1765                                   <property name="use_underline">True</property>
1766                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1767                                   <property name="focus_on_click">True</property>
1768                                 </widget>
1769                                 <packing>
1770                                   <property name="left_attach">0</property>
1771                                   <property name="right_attach">1</property>
1772                                   <property name="top_attach">14</property>
1773                                   <property name="bottom_attach">15</property>
1774                                   <property name="x_options">fill</property>
1775                                   <property name="y_options"></property>
1776                                 </packing>
1777                               </child>
1778
1779                               <child>
1780                                 <widget class="GtkButton" id="autoButton">
1781                                   <property name="visible">True</property>
1782                                   <property name="tooltip" translatable="yes">Auto</property>
1783                                   <property name="can_focus">True</property>
1784                                   <property name="label" translatable="yes">auto</property>
1785                                   <property name="use_underline">True</property>
1786                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1787                                   <property name="focus_on_click">True</property>
1788                                 </widget>
1789                                 <packing>
1790                                   <property name="left_attach">1</property>
1791                                   <property name="right_attach">2</property>
1792                                   <property name="top_attach">14</property>
1793                                   <property name="bottom_attach">15</property>
1794                                   <property name="x_options">fill</property>
1795                                   <property name="y_options"></property>
1796                                 </packing>
1797                               </child>
1798
1799                               <child>
1800                                 <widget class="GtkButton" id="cutButton">
1801                                   <property name="visible">True</property>
1802                                   <property name="tooltip" translatable="yes">Cut</property>
1803                                   <property name="can_focus">True</property>
1804                                   <property name="label" translatable="yes">cut</property>
1805                                   <property name="use_underline">True</property>
1806                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1807                                   <property name="focus_on_click">True</property>
1808                                 </widget>
1809                                 <packing>
1810                                   <property name="left_attach">0</property>
1811                                   <property name="right_attach">1</property>
1812                                   <property name="top_attach">16</property>
1813                                   <property name="bottom_attach">17</property>
1814                                   <property name="x_options">fill</property>
1815                                   <property name="y_options"></property>
1816                                 </packing>
1817                               </child>
1818
1819                               <child>
1820                                 <widget class="GtkButton" id="replaceButton">
1821                                   <property name="visible">True</property>
1822                                   <property name="tooltip" translatable="yes">Replace</property>
1823                                   <property name="can_focus">True</property>
1824                                   <property name="label" translatable="yes">repl</property>
1825                                   <property name="use_underline">True</property>
1826                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1827                                   <property name="focus_on_click">True</property>
1828                                 </widget>
1829                                 <packing>
1830                                   <property name="left_attach">1</property>
1831                                   <property name="right_attach">2</property>
1832                                   <property name="top_attach">16</property>
1833                                   <property name="bottom_attach">17</property>
1834                                   <property name="x_options">fill</property>
1835                                   <property name="y_options"></property>
1836                                 </packing>
1837                               </child>
1838
1839                               <child>
1840                                 <widget class="GtkButton" id="elimTypeButton">
1841                                   <property name="visible">True</property>
1842                                   <property name="tooltip" translatable="yes">ElimType</property>
1843                                   <property name="can_focus">True</property>
1844                                   <property name="label" translatable="yes">elimTy</property>
1845                                   <property name="use_underline">True</property>
1846                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1847                                   <property name="focus_on_click">True</property>
1848                                 </widget>
1849                                 <packing>
1850                                   <property name="left_attach">1</property>
1851                                   <property name="right_attach">2</property>
1852                                   <property name="top_attach">4</property>
1853                                   <property name="bottom_attach">5</property>
1854                                   <property name="x_options">fill</property>
1855                                   <property name="y_options"></property>
1856                                 </packing>
1857                               </child>
1858
1859                               <child>
1860                                 <widget class="GtkHBox" id="hbox18">
1861                                   <property name="visible">True</property>
1862                                   <property name="homogeneous">True</property>
1863                                   <property name="spacing">0</property>
1864
1865                                   <child>
1866                                     <widget class="GtkButton" id="rightButton">
1867                                       <property name="visible">True</property>
1868                                       <property name="tooltip" translatable="yes">Right</property>
1869                                       <property name="can_focus">True</property>
1870                                       <property name="label" translatable="yes">R</property>
1871                                       <property name="use_underline">True</property>
1872                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1873                                       <property name="focus_on_click">True</property>
1874                                     </widget>
1875                                     <packing>
1876                                       <property name="padding">0</property>
1877                                       <property name="expand">True</property>
1878                                       <property name="fill">True</property>
1879                                     </packing>
1880                                   </child>
1881
1882                                   <child>
1883                                     <widget class="GtkButton" id="existsButton">
1884                                       <property name="visible">True</property>
1885                                       <property name="tooltip" translatable="yes">Exists</property>
1886                                       <property name="can_focus">True</property>
1887                                       <property name="label" translatable="yes">∃</property>
1888                                       <property name="use_underline">True</property>
1889                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1890                                       <property name="focus_on_click">True</property>
1891                                     </widget>
1892                                     <packing>
1893                                       <property name="padding">0</property>
1894                                       <property name="expand">True</property>
1895                                       <property name="fill">True</property>
1896                                     </packing>
1897                                   </child>
1898                                 </widget>
1899                                 <packing>
1900                                   <property name="left_attach">1</property>
1901                                   <property name="right_attach">2</property>
1902                                   <property name="top_attach">6</property>
1903                                   <property name="bottom_attach">7</property>
1904                                   <property name="x_options">fill</property>
1905                                   <property name="y_options">fill</property>
1906                                 </packing>
1907                               </child>
1908
1909                               <child>
1910                                 <widget class="GtkHBox" id="hbox17">
1911                                   <property name="visible">True</property>
1912                                   <property name="homogeneous">True</property>
1913                                   <property name="spacing">0</property>
1914
1915                                   <child>
1916                                     <widget class="GtkButton" id="splitButton">
1917                                       <property name="visible">True</property>
1918                                       <property name="tooltip" translatable="yes">Split</property>
1919                                       <property name="can_focus">True</property>
1920                                       <property name="label" translatable="yes">∧</property>
1921                                       <property name="use_underline">True</property>
1922                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1923                                       <property name="focus_on_click">True</property>
1924                                     </widget>
1925                                     <packing>
1926                                       <property name="padding">0</property>
1927                                       <property name="expand">True</property>
1928                                       <property name="fill">True</property>
1929                                     </packing>
1930                                   </child>
1931
1932                                   <child>
1933                                     <widget class="GtkButton" id="leftButton">
1934                                       <property name="visible">True</property>
1935                                       <property name="tooltip" translatable="yes">Left</property>
1936                                       <property name="can_focus">True</property>
1937                                       <property name="label" translatable="yes">L</property>
1938                                       <property name="use_underline">True</property>
1939                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1940                                       <property name="focus_on_click">True</property>
1941                                     </widget>
1942                                     <packing>
1943                                       <property name="padding">0</property>
1944                                       <property name="expand">True</property>
1945                                       <property name="fill">True</property>
1946                                     </packing>
1947                                   </child>
1948                                 </widget>
1949                                 <packing>
1950                                   <property name="left_attach">0</property>
1951                                   <property name="right_attach">1</property>
1952                                   <property name="top_attach">6</property>
1953                                   <property name="bottom_attach">7</property>
1954                                   <property name="x_options">fill</property>
1955                                   <property name="y_options">fill</property>
1956                                 </packing>
1957                               </child>
1958
1959                               <child>
1960                                 <widget class="GtkAlignment" id="alignment6">
1961                                   <property name="visible">True</property>
1962                                   <property name="xalign">0.5</property>
1963                                   <property name="yalign">0.5</property>
1964                                   <property name="xscale">1</property>
1965                                   <property name="yscale">1</property>
1966                                   <property name="top_padding">0</property>
1967                                   <property name="bottom_padding">0</property>
1968                                   <property name="left_padding">0</property>
1969                                   <property name="right_padding">0</property>
1970
1971                                   <child>
1972                                     <placeholder/>
1973                                   </child>
1974                                 </widget>
1975                                 <packing>
1976                                   <property name="left_attach">0</property>
1977                                   <property name="right_attach">1</property>
1978                                   <property name="top_attach">1</property>
1979                                   <property name="bottom_attach">2</property>
1980                                   <property name="x_options">fill</property>
1981                                 </packing>
1982                               </child>
1983
1984                               <child>
1985                                 <widget class="GtkAlignment" id="alignment7">
1986                                   <property name="visible">True</property>
1987                                   <property name="xalign">0.5</property>
1988                                   <property name="yalign">0.5</property>
1989                                   <property name="xscale">1</property>
1990                                   <property name="yscale">1</property>
1991                                   <property name="top_padding">0</property>
1992                                   <property name="bottom_padding">0</property>
1993                                   <property name="left_padding">0</property>
1994                                   <property name="right_padding">0</property>
1995
1996                                   <child>
1997                                     <placeholder/>
1998                                   </child>
1999                                 </widget>
2000                                 <packing>
2001                                   <property name="left_attach">0</property>
2002                                   <property name="right_attach">1</property>
2003                                   <property name="top_attach">3</property>
2004                                   <property name="bottom_attach">4</property>
2005                                   <property name="x_options">fill</property>
2006                                 </packing>
2007                               </child>
2008
2009                               <child>
2010                                 <widget class="GtkAlignment" id="alignment8">
2011                                   <property name="visible">True</property>
2012                                   <property name="xalign">0.5</property>
2013                                   <property name="yalign">0.5</property>
2014                                   <property name="xscale">1</property>
2015                                   <property name="yscale">1</property>
2016                                   <property name="top_padding">0</property>
2017                                   <property name="bottom_padding">0</property>
2018                                   <property name="left_padding">0</property>
2019                                   <property name="right_padding">0</property>
2020
2021                                   <child>
2022                                     <placeholder/>
2023                                   </child>
2024                                 </widget>
2025                                 <packing>
2026                                   <property name="left_attach">0</property>
2027                                   <property name="right_attach">1</property>
2028                                   <property name="top_attach">5</property>
2029                                   <property name="bottom_attach">6</property>
2030                                   <property name="x_options">fill</property>
2031                                 </packing>
2032                               </child>
2033
2034                               <child>
2035                                 <widget class="GtkAlignment" id="alignment9">
2036                                   <property name="visible">True</property>
2037                                   <property name="xalign">0.5</property>
2038                                   <property name="yalign">0.5</property>
2039                                   <property name="xscale">1</property>
2040                                   <property name="yscale">1</property>
2041                                   <property name="top_padding">0</property>
2042                                   <property name="bottom_padding">0</property>
2043                                   <property name="left_padding">0</property>
2044                                   <property name="right_padding">0</property>
2045
2046                                   <child>
2047                                     <placeholder/>
2048                                   </child>
2049                                 </widget>
2050                                 <packing>
2051                                   <property name="left_attach">0</property>
2052                                   <property name="right_attach">1</property>
2053                                   <property name="top_attach">7</property>
2054                                   <property name="bottom_attach">8</property>
2055                                   <property name="x_options">fill</property>
2056                                 </packing>
2057                               </child>
2058
2059                               <child>
2060                                 <widget class="GtkAlignment" id="alignment10">
2061                                   <property name="visible">True</property>
2062                                   <property name="xalign">0.5</property>
2063                                   <property name="yalign">0.5</property>
2064                                   <property name="xscale">1</property>
2065                                   <property name="yscale">1</property>
2066                                   <property name="top_padding">0</property>
2067                                   <property name="bottom_padding">0</property>
2068                                   <property name="left_padding">0</property>
2069                                   <property name="right_padding">0</property>
2070
2071                                   <child>
2072                                     <placeholder/>
2073                                   </child>
2074                                 </widget>
2075                                 <packing>
2076                                   <property name="left_attach">0</property>
2077                                   <property name="right_attach">1</property>
2078                                   <property name="top_attach">10</property>
2079                                   <property name="bottom_attach">11</property>
2080                                   <property name="x_options">fill</property>
2081                                 </packing>
2082                               </child>
2083
2084                               <child>
2085                                 <widget class="GtkAlignment" id="alignment11">
2086                                   <property name="visible">True</property>
2087                                   <property name="xalign">0.5</property>
2088                                   <property name="yalign">0.5</property>
2089                                   <property name="xscale">1</property>
2090                                   <property name="yscale">1</property>
2091                                   <property name="top_padding">0</property>
2092                                   <property name="bottom_padding">0</property>
2093                                   <property name="left_padding">0</property>
2094                                   <property name="right_padding">0</property>
2095
2096                                   <child>
2097                                     <placeholder/>
2098                                   </child>
2099                                 </widget>
2100                                 <packing>
2101                                   <property name="left_attach">0</property>
2102                                   <property name="right_attach">1</property>
2103                                   <property name="top_attach">13</property>
2104                                   <property name="bottom_attach">14</property>
2105                                   <property name="x_options">fill</property>
2106                                 </packing>
2107                               </child>
2108
2109                               <child>
2110                                 <widget class="GtkAlignment" id="alignment12">
2111                                   <property name="visible">True</property>
2112                                   <property name="xalign">0.5</property>
2113                                   <property name="yalign">0.5</property>
2114                                   <property name="xscale">1</property>
2115                                   <property name="yscale">1</property>
2116                                   <property name="top_padding">0</property>
2117                                   <property name="bottom_padding">0</property>
2118                                   <property name="left_padding">0</property>
2119                                   <property name="right_padding">0</property>
2120
2121                                   <child>
2122                                     <placeholder/>
2123                                   </child>
2124                                 </widget>
2125                                 <packing>
2126                                   <property name="left_attach">0</property>
2127                                   <property name="right_attach">1</property>
2128                                   <property name="top_attach">15</property>
2129                                   <property name="bottom_attach">16</property>
2130                                   <property name="x_options">fill</property>
2131                                 </packing>
2132                               </child>
2133                             </widget>
2134                           </child>
2135                         </widget>
2136                         <packing>
2137                           <property name="padding">0</property>
2138                           <property name="expand">False</property>
2139                           <property name="fill">True</property>
2140                         </packing>
2141                       </child>
2142
2143                       <child>
2144                         <widget class="GtkVBox" id="vboxScript">
2145                           <property name="width_request">400</property>
2146                           <property name="visible">True</property>
2147                           <property name="homogeneous">False</property>
2148                           <property name="spacing">0</property>
2149
2150                           <child>
2151                             <widget class="GtkHBox" id="hbox28">
2152                               <property name="visible">True</property>
2153                               <property name="homogeneous">False</property>
2154                               <property name="spacing">0</property>
2155
2156                               <child>
2157                                 <widget class="GtkToolbar" id="buttonsToolbar">
2158                                   <property name="visible">True</property>
2159                                   <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
2160                                   <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
2161                                   <property name="tooltips">True</property>
2162                                   <property name="show_arrow">True</property>
2163
2164                                   <child>
2165                                     <widget class="GtkToolItem" id="toolitem41">
2166                                       <property name="visible">True</property>
2167                                       <property name="visible_horizontal">True</property>
2168                                       <property name="visible_vertical">True</property>
2169                                       <property name="is_important">False</property>
2170
2171                                       <child>
2172                                         <widget class="GtkButton" id="scriptTopButton">
2173                                           <property name="visible">True</property>
2174                                           <property name="tooltip" translatable="yes">Restart</property>
2175                                           <property name="can_focus">True</property>
2176                                           <property name="relief">GTK_RELIEF_NONE</property>
2177                                           <property name="focus_on_click">True</property>
2178
2179                                           <child>
2180                                             <widget class="GtkImage" id="image920">
2181                                               <property name="visible">True</property>
2182                                               <property name="stock">gtk-goto-top</property>
2183                                               <property name="icon_size">4</property>
2184                                               <property name="xalign">0.5</property>
2185                                               <property name="yalign">0.5</property>
2186                                               <property name="xpad">0</property>
2187                                               <property name="ypad">0</property>
2188                                             </widget>
2189                                           </child>
2190                                         </widget>
2191                                       </child>
2192                                     </widget>
2193                                     <packing>
2194                                       <property name="expand">False</property>
2195                                       <property name="homogeneous">False</property>
2196                                     </packing>
2197                                   </child>
2198
2199                                   <child>
2200                                     <widget class="GtkToolItem" id="toolitem42">
2201                                       <property name="visible">True</property>
2202                                       <property name="visible_horizontal">True</property>
2203                                       <property name="visible_vertical">True</property>
2204                                       <property name="is_important">False</property>
2205
2206                                       <child>
2207                                         <widget class="GtkButton" id="scriptRetractButton">
2208                                           <property name="visible">True</property>
2209                                           <property name="tooltip" translatable="yes">Retract 1 phrase</property>
2210                                           <property name="can_focus">True</property>
2211                                           <property name="relief">GTK_RELIEF_NONE</property>
2212                                           <property name="focus_on_click">True</property>
2213
2214                                           <child>
2215                                             <widget class="GtkImage" id="image921">
2216                                               <property name="visible">True</property>
2217                                               <property name="stock">gtk-go-up</property>
2218                                               <property name="icon_size">4</property>
2219                                               <property name="xalign">0.5</property>
2220                                               <property name="yalign">0.5</property>
2221                                               <property name="xpad">0</property>
2222                                               <property name="ypad">0</property>
2223                                             </widget>
2224                                           </child>
2225                                         </widget>
2226                                       </child>
2227                                     </widget>
2228                                     <packing>
2229                                       <property name="expand">False</property>
2230                                       <property name="homogeneous">False</property>
2231                                     </packing>
2232                                   </child>
2233
2234                                   <child>
2235                                     <widget class="GtkToolItem" id="toolitem43">
2236                                       <property name="visible">True</property>
2237                                       <property name="visible_horizontal">True</property>
2238                                       <property name="visible_vertical">True</property>
2239                                       <property name="is_important">False</property>
2240
2241                                       <child>
2242                                         <widget class="GtkButton" id="scriptJumpButton">
2243                                           <property name="visible">True</property>
2244                                           <property name="tooltip" translatable="yes">Execute until point</property>
2245                                           <property name="can_focus">True</property>
2246                                           <property name="relief">GTK_RELIEF_NONE</property>
2247                                           <property name="focus_on_click">True</property>
2248
2249                                           <child>
2250                                             <widget class="GtkImage" id="image922">
2251                                               <property name="visible">True</property>
2252                                               <property name="stock">gtk-jump-to</property>
2253                                               <property name="icon_size">4</property>
2254                                               <property name="xalign">0.5</property>
2255                                               <property name="yalign">0.5</property>
2256                                               <property name="xpad">0</property>
2257                                               <property name="ypad">0</property>
2258                                             </widget>
2259                                           </child>
2260                                         </widget>
2261                                       </child>
2262                                     </widget>
2263                                     <packing>
2264                                       <property name="expand">False</property>
2265                                       <property name="homogeneous">False</property>
2266                                     </packing>
2267                                   </child>
2268
2269                                   <child>
2270                                     <widget class="GtkToolItem" id="toolitem44">
2271                                       <property name="visible">True</property>
2272                                       <property name="visible_horizontal">True</property>
2273                                       <property name="visible_vertical">True</property>
2274                                       <property name="is_important">False</property>
2275
2276                                       <child>
2277                                         <widget class="GtkButton" id="scriptAdvanceButton">
2278                                           <property name="visible">True</property>
2279                                           <property name="tooltip" translatable="yes">Execute 1 phrase</property>
2280                                           <property name="can_focus">True</property>
2281                                           <property name="relief">GTK_RELIEF_NONE</property>
2282                                           <property name="focus_on_click">True</property>
2283
2284                                           <child>
2285                                             <widget class="GtkImage" id="image923">
2286                                               <property name="visible">True</property>
2287                                               <property name="stock">gtk-go-down</property>
2288                                               <property name="icon_size">4</property>
2289                                               <property name="xalign">0.5</property>
2290                                               <property name="yalign">0.5</property>
2291                                               <property name="xpad">0</property>
2292                                               <property name="ypad">0</property>
2293                                             </widget>
2294                                           </child>
2295                                         </widget>
2296                                       </child>
2297                                     </widget>
2298                                     <packing>
2299                                       <property name="expand">False</property>
2300                                       <property name="homogeneous">False</property>
2301                                     </packing>
2302                                   </child>
2303
2304                                   <child>
2305                                     <widget class="GtkToolItem" id="toolitem45">
2306                                       <property name="visible">True</property>
2307                                       <property name="visible_horizontal">True</property>
2308                                       <property name="visible_vertical">True</property>
2309                                       <property name="is_important">False</property>
2310
2311                                       <child>
2312                                         <widget class="GtkButton" id="scriptBottomButton">
2313                                           <property name="visible">True</property>
2314                                           <property name="tooltip" translatable="yes">Execute all</property>
2315                                           <property name="can_focus">True</property>
2316                                           <property name="relief">GTK_RELIEF_NONE</property>
2317                                           <property name="focus_on_click">True</property>
2318
2319                                           <child>
2320                                             <widget class="GtkImage" id="image924">
2321                                               <property name="visible">True</property>
2322                                               <property name="stock">gtk-goto-bottom</property>
2323                                               <property name="icon_size">4</property>
2324                                               <property name="xalign">0.5</property>
2325                                               <property name="yalign">0.5</property>
2326                                               <property name="xpad">0</property>
2327                                               <property name="ypad">0</property>
2328                                             </widget>
2329                                           </child>
2330                                         </widget>
2331                                       </child>
2332                                     </widget>
2333                                     <packing>
2334                                       <property name="expand">False</property>
2335                                       <property name="homogeneous">False</property>
2336                                     </packing>
2337                                   </child>
2338                                 </widget>
2339                                 <packing>
2340                                   <property name="padding">0</property>
2341                                   <property name="expand">True</property>
2342                                   <property name="fill">True</property>
2343                                 </packing>
2344                               </child>
2345
2346                               <child>
2347                                 <widget class="GtkToolItem" id="toolitemxx">
2348                                   <property name="visible">True</property>
2349                                   <property name="visible_horizontal">True</property>
2350                                   <property name="visible_vertical">True</property>
2351                                   <property name="is_important">False</property>
2352
2353                                   <child>
2354                                     <widget class="GtkButton" id="scriptAbortButton">
2355                                       <property name="visible">True</property>
2356                                       <property name="tooltip" translatable="yes">Abort</property>
2357                                       <property name="can_focus">True</property>
2358                                       <property name="relief">GTK_RELIEF_NONE</property>
2359                                       <property name="focus_on_click">True</property>
2360
2361                                       <child>
2362                                         <widget class="GtkImage" id="image925">
2363                                           <property name="visible">True</property>
2364                                           <property name="stock">gtk-cancel</property>
2365                                           <property name="icon_size">4</property>
2366                                           <property name="xalign">0.5</property>
2367                                           <property name="yalign">0.5</property>
2368                                           <property name="xpad">0</property>
2369                                           <property name="ypad">0</property>
2370                                           <accessibility>
2371                                             <atkproperty name="AtkObject::accessible_name" translatable="yes">abort</atkproperty>
2372                                           </accessibility>
2373                                         </widget>
2374                                       </child>
2375                                     </widget>
2376                                   </child>
2377                                 </widget>
2378                                 <packing>
2379                                   <property name="padding">0</property>
2380                                   <property name="expand">False</property>
2381                                   <property name="fill">False</property>
2382                                 </packing>
2383                               </child>
2384                             </widget>
2385                             <packing>
2386                               <property name="padding">0</property>
2387                               <property name="expand">False</property>
2388                               <property name="fill">False</property>
2389                             </packing>
2390                           </child>
2391
2392                           <child>
2393                             <widget class="GtkNotebook" id="scriptNotebook">
2394                               <property name="visible">True</property>
2395                               <property name="can_focus">True</property>
2396                               <property name="show_tabs">True</property>
2397                               <property name="show_border">True</property>
2398                               <property name="tab_pos">GTK_POS_BOTTOM</property>
2399                               <property name="scrollable">False</property>
2400                               <property name="enable_popup">False</property>
2401
2402                               <child>
2403                                 <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
2404                                   <property name="visible">True</property>
2405                                   <property name="can_focus">True</property>
2406                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2407                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2408                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2409                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2410
2411                                   <child>
2412                                     <placeholder/>
2413                                   </child>
2414                                 </widget>
2415                                 <packing>
2416                                   <property name="tab_expand">False</property>
2417                                   <property name="tab_fill">True</property>
2418                                 </packing>
2419                               </child>
2420
2421                               <child>
2422                                 <widget class="GtkLabel" id="scriptLabel">
2423                                   <property name="visible">True</property>
2424                                   <property name="label" translatable="yes">script</property>
2425                                   <property name="use_underline">False</property>
2426                                   <property name="use_markup">False</property>
2427                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2428                                   <property name="wrap">False</property>
2429                                   <property name="selectable">False</property>
2430                                   <property name="xalign">0.5</property>
2431                                   <property name="yalign">0.5</property>
2432                                   <property name="xpad">0</property>
2433                                   <property name="ypad">0</property>
2434                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2435                                   <property name="width_chars">-1</property>
2436                                   <property name="single_line_mode">False</property>
2437                                   <property name="angle">0</property>
2438                                 </widget>
2439                                 <packing>
2440                                   <property name="type">tab</property>
2441                                 </packing>
2442                               </child>
2443
2444                               <child>
2445                                 <widget class="GtkScrolledWindow" id="scrolledwindow8">
2446                                   <property name="visible">True</property>
2447                                   <property name="can_focus">True</property>
2448                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2449                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2450                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2451                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2452
2453                                   <child>
2454                                     <widget class="GtkViewport" id="viewport1">
2455                                       <property name="visible">True</property>
2456                                       <property name="shadow_type">GTK_SHADOW_IN</property>
2457
2458                                       <child>
2459                                         <widget class="GtkLabel" id="label25">
2460                                           <property name="visible">True</property>
2461                                           <property name="label" translatable="yes">Not implemented.</property>
2462                                           <property name="use_underline">False</property>
2463                                           <property name="use_markup">False</property>
2464                                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2465                                           <property name="wrap">False</property>
2466                                           <property name="selectable">False</property>
2467                                           <property name="xalign">0.5</property>
2468                                           <property name="yalign">0.5</property>
2469                                           <property name="xpad">0</property>
2470                                           <property name="ypad">0</property>
2471                                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2472                                           <property name="width_chars">-1</property>
2473                                           <property name="single_line_mode">False</property>
2474                                           <property name="angle">0</property>
2475                                         </widget>
2476                                       </child>
2477                                     </widget>
2478                                   </child>
2479                                 </widget>
2480                                 <packing>
2481                                   <property name="tab_expand">False</property>
2482                                   <property name="tab_fill">True</property>
2483                                 </packing>
2484                               </child>
2485
2486                               <child>
2487                                 <widget class="GtkLabel" id="label13">
2488                                   <property name="visible">True</property>
2489                                   <property name="label" translatable="yes">outline</property>
2490                                   <property name="use_underline">False</property>
2491                                   <property name="use_markup">False</property>
2492                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2493                                   <property name="wrap">False</property>
2494                                   <property name="selectable">False</property>
2495                                   <property name="xalign">0.5</property>
2496                                   <property name="yalign">0.5</property>
2497                                   <property name="xpad">0</property>
2498                                   <property name="ypad">0</property>
2499                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2500                                   <property name="width_chars">-1</property>
2501                                   <property name="single_line_mode">False</property>
2502                                   <property name="angle">0</property>
2503                                 </widget>
2504                                 <packing>
2505                                   <property name="type">tab</property>
2506                                 </packing>
2507                               </child>
2508                             </widget>
2509                             <packing>
2510                               <property name="padding">0</property>
2511                               <property name="expand">True</property>
2512                               <property name="fill">True</property>
2513                             </packing>
2514                           </child>
2515                         </widget>
2516                         <packing>
2517                           <property name="padding">0</property>
2518                           <property name="expand">True</property>
2519                           <property name="fill">True</property>
2520                         </packing>
2521                       </child>
2522                     </widget>
2523                     <packing>
2524                       <property name="shrink">True</property>
2525                       <property name="resize">False</property>
2526                     </packing>
2527                   </child>
2528
2529                   <child>
2530                     <widget class="GtkVPaned" id="vpaned1">
2531                       <property name="width_request">250</property>
2532                       <property name="height_request">500</property>
2533                       <property name="visible">True</property>
2534                       <property name="can_focus">True</property>
2535                       <property name="position">380</property>
2536
2537                       <child>
2538                         <widget class="GtkNotebook" id="sequentsNotebook">
2539                           <property name="visible">True</property>
2540                           <property name="can_focus">True</property>
2541                           <property name="show_tabs">True</property>
2542                           <property name="show_border">True</property>
2543                           <property name="tab_pos">GTK_POS_TOP</property>
2544                           <property name="scrollable">False</property>
2545                           <property name="enable_popup">False</property>
2546                         </widget>
2547                         <packing>
2548                           <property name="shrink">True</property>
2549                           <property name="resize">False</property>
2550                         </packing>
2551                       </child>
2552
2553                       <child>
2554                         <widget class="GtkHBox" id="hbox9">
2555                           <property name="visible">True</property>
2556                           <property name="homogeneous">False</property>
2557                           <property name="spacing">0</property>
2558
2559                           <child>
2560                             <widget class="GtkScrolledWindow" id="logScrolledWin">
2561                               <property name="visible">True</property>
2562                               <property name="can_focus">True</property>
2563                               <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
2564                               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2565                               <property name="shadow_type">GTK_SHADOW_IN</property>
2566                               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2567
2568                               <child>
2569                                 <widget class="GtkTextView" id="logTextView">
2570                                   <property name="visible">True</property>
2571                                   <property name="can_focus">True</property>
2572                                   <property name="editable">False</property>
2573                                   <property name="overwrite">False</property>
2574                                   <property name="accepts_tab">True</property>
2575                                   <property name="justification">GTK_JUSTIFY_LEFT</property>
2576                                   <property name="wrap_mode">GTK_WRAP_CHAR</property>
2577                                   <property name="cursor_visible">False</property>
2578                                   <property name="pixels_above_lines">0</property>
2579                                   <property name="pixels_below_lines">0</property>
2580                                   <property name="pixels_inside_wrap">0</property>
2581                                   <property name="left_margin">0</property>
2582                                   <property name="right_margin">0</property>
2583                                   <property name="indent">0</property>
2584                                   <property name="text" translatable="yes"></property>
2585                                 </widget>
2586                               </child>
2587                             </widget>
2588                             <packing>
2589                               <property name="padding">0</property>
2590                               <property name="expand">True</property>
2591                               <property name="fill">True</property>
2592                             </packing>
2593                           </child>
2594                         </widget>
2595                         <packing>
2596                           <property name="shrink">True</property>
2597                           <property name="resize">True</property>
2598                         </packing>
2599                       </child>
2600                     </widget>
2601                     <packing>
2602                       <property name="shrink">True</property>
2603                       <property name="resize">True</property>
2604                     </packing>
2605                   </child>
2606                 </widget>
2607                 <packing>
2608                   <property name="padding">0</property>
2609                   <property name="expand">True</property>
2610                   <property name="fill">True</property>
2611                 </packing>
2612               </child>
2613             </widget>
2614             <packing>
2615               <property name="padding">0</property>
2616               <property name="expand">True</property>
2617               <property name="fill">True</property>
2618             </packing>
2619           </child>
2620
2621           <child>
2622             <widget class="GtkHBox" id="hbox10">
2623               <property name="visible">True</property>
2624               <property name="homogeneous">False</property>
2625               <property name="spacing">0</property>
2626
2627               <child>
2628                 <widget class="GtkStatusbar" id="StatusBar">
2629                   <property name="visible">True</property>
2630                   <property name="has_resize_grip">False</property>
2631                 </widget>
2632                 <packing>
2633                   <property name="padding">0</property>
2634                   <property name="expand">True</property>
2635                   <property name="fill">True</property>
2636                 </packing>
2637               </child>
2638
2639               <child>
2640                 <widget class="GtkNotebook" id="HintNotebook">
2641                   <property name="visible">True</property>
2642                   <property name="show_tabs">False</property>
2643                   <property name="show_border">True</property>
2644                   <property name="tab_pos">GTK_POS_TOP</property>
2645                   <property name="scrollable">False</property>
2646                   <property name="enable_popup">False</property>
2647
2648                   <child>
2649                     <widget class="GtkImage" id="HintLowImage">
2650                       <property name="visible">True</property>
2651                       <property name="xalign">0.5</property>
2652                       <property name="yalign">0.5</property>
2653                       <property name="xpad">0</property>
2654                       <property name="ypad">0</property>
2655                     </widget>
2656                     <packing>
2657                       <property name="tab_expand">False</property>
2658                       <property name="tab_fill">True</property>
2659                     </packing>
2660                   </child>
2661
2662                   <child>
2663                     <widget class="GtkLabel" id="label14">
2664                       <property name="visible">True</property>
2665                       <property name="label" translatable="yes">label14</property>
2666                       <property name="use_underline">False</property>
2667                       <property name="use_markup">False</property>
2668                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2669                       <property name="wrap">False</property>
2670                       <property name="selectable">False</property>
2671                       <property name="xalign">0.5</property>
2672                       <property name="yalign">0.5</property>
2673                       <property name="xpad">0</property>
2674                       <property name="ypad">0</property>
2675                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2676                       <property name="width_chars">-1</property>
2677                       <property name="single_line_mode">False</property>
2678                       <property name="angle">0</property>
2679                     </widget>
2680                     <packing>
2681                       <property name="type">tab</property>
2682                     </packing>
2683                   </child>
2684
2685                   <child>
2686                     <widget class="GtkImage" id="HintMediumImage">
2687                       <property name="visible">True</property>
2688                       <property name="xalign">0.5</property>
2689                       <property name="yalign">0.5</property>
2690                       <property name="xpad">0</property>
2691                       <property name="ypad">0</property>
2692                     </widget>
2693                     <packing>
2694                       <property name="tab_expand">False</property>
2695                       <property name="tab_fill">True</property>
2696                     </packing>
2697                   </child>
2698
2699                   <child>
2700                     <widget class="GtkLabel" id="label15">
2701                       <property name="visible">True</property>
2702                       <property name="label" translatable="yes">label15</property>
2703                       <property name="use_underline">False</property>
2704                       <property name="use_markup">False</property>
2705                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2706                       <property name="wrap">False</property>
2707                       <property name="selectable">False</property>
2708                       <property name="xalign">0.5</property>
2709                       <property name="yalign">0.5</property>
2710                       <property name="xpad">0</property>
2711                       <property name="ypad">0</property>
2712                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2713                       <property name="width_chars">-1</property>
2714                       <property name="single_line_mode">False</property>
2715                       <property name="angle">0</property>
2716                     </widget>
2717                     <packing>
2718                       <property name="type">tab</property>
2719                     </packing>
2720                   </child>
2721
2722                   <child>
2723                     <widget class="GtkImage" id="HintHighImage">
2724                       <property name="visible">True</property>
2725                       <property name="xalign">0.5</property>
2726                       <property name="yalign">0.5</property>
2727                       <property name="xpad">0</property>
2728                       <property name="ypad">0</property>
2729                     </widget>
2730                     <packing>
2731                       <property name="tab_expand">False</property>
2732                       <property name="tab_fill">True</property>
2733                     </packing>
2734                   </child>
2735
2736                   <child>
2737                     <widget class="GtkLabel" id="label16">
2738                       <property name="visible">True</property>
2739                       <property name="label" translatable="yes">label16</property>
2740                       <property name="use_underline">False</property>
2741                       <property name="use_markup">False</property>
2742                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2743                       <property name="wrap">False</property>
2744                       <property name="selectable">False</property>
2745                       <property name="xalign">0.5</property>
2746                       <property name="yalign">0.5</property>
2747                       <property name="xpad">0</property>
2748                       <property name="ypad">0</property>
2749                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2750                       <property name="width_chars">-1</property>
2751                       <property name="single_line_mode">False</property>
2752                       <property name="angle">0</property>
2753                     </widget>
2754                     <packing>
2755                       <property name="type">tab</property>
2756                     </packing>
2757                   </child>
2758                 </widget>
2759                 <packing>
2760                   <property name="padding">0</property>
2761                   <property name="expand">False</property>
2762                   <property name="fill">True</property>
2763                 </packing>
2764               </child>
2765             </widget>
2766             <packing>
2767               <property name="padding">0</property>
2768               <property name="expand">False</property>
2769               <property name="fill">False</property>
2770             </packing>
2771           </child>
2772         </widget>
2773       </child>
2774     </widget>
2775   </child>
2776 </widget>
2777
2778 <widget class="GtkDialog" id="TextDialog">
2779   <property name="title" translatable="yes">DUMMY</property>
2780   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2781   <property name="window_position">GTK_WIN_POS_NONE</property>
2782   <property name="modal">False</property>
2783   <property name="resizable">True</property>
2784   <property name="destroy_with_parent">False</property>
2785   <property name="decorated">True</property>
2786   <property name="skip_taskbar_hint">False</property>
2787   <property name="skip_pager_hint">False</property>
2788   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2789   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2790   <property name="focus_on_map">True</property>
2791   <property name="urgency_hint">False</property>
2792   <property name="has_separator">True</property>
2793
2794   <child internal-child="vbox">
2795     <widget class="GtkVBox" id="vbox5">
2796       <property name="visible">True</property>
2797       <property name="homogeneous">False</property>
2798       <property name="spacing">0</property>
2799
2800       <child internal-child="action_area">
2801         <widget class="GtkHButtonBox" id="hbuttonbox1">
2802           <property name="visible">True</property>
2803           <property name="layout_style">GTK_BUTTONBOX_END</property>
2804
2805           <child>
2806             <widget class="GtkButton" id="TextDialogCancelButton">
2807               <property name="visible">True</property>
2808               <property name="can_default">True</property>
2809               <property name="can_focus">True</property>
2810               <property name="label">gtk-cancel</property>
2811               <property name="use_stock">True</property>
2812               <property name="relief">GTK_RELIEF_NORMAL</property>
2813               <property name="focus_on_click">True</property>
2814               <property name="response_id">-6</property>
2815             </widget>
2816           </child>
2817
2818           <child>
2819             <widget class="GtkButton" id="TextDialogOkButton">
2820               <property name="visible">True</property>
2821               <property name="can_default">True</property>
2822               <property name="can_focus">True</property>
2823               <property name="label">gtk-ok</property>
2824               <property name="use_stock">True</property>
2825               <property name="relief">GTK_RELIEF_NORMAL</property>
2826               <property name="focus_on_click">True</property>
2827               <property name="response_id">-5</property>
2828             </widget>
2829           </child>
2830         </widget>
2831         <packing>
2832           <property name="padding">0</property>
2833           <property name="expand">False</property>
2834           <property name="fill">True</property>
2835           <property name="pack_type">GTK_PACK_END</property>
2836         </packing>
2837       </child>
2838
2839       <child>
2840         <widget class="GtkLabel" id="TextDialogLabel">
2841           <property name="visible">True</property>
2842           <property name="label" translatable="yes">DUMMY</property>
2843           <property name="use_underline">False</property>
2844           <property name="use_markup">False</property>
2845           <property name="justify">GTK_JUSTIFY_LEFT</property>
2846           <property name="wrap">False</property>
2847           <property name="selectable">False</property>
2848           <property name="xalign">0.5</property>
2849           <property name="yalign">0.5</property>
2850           <property name="xpad">0</property>
2851           <property name="ypad">0</property>
2852           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2853           <property name="width_chars">-1</property>
2854           <property name="single_line_mode">False</property>
2855           <property name="angle">0</property>
2856         </widget>
2857         <packing>
2858           <property name="padding">0</property>
2859           <property name="expand">False</property>
2860           <property name="fill">False</property>
2861         </packing>
2862       </child>
2863
2864       <child>
2865         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2866           <property name="visible">True</property>
2867           <property name="can_focus">True</property>
2868           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2869           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2870           <property name="shadow_type">GTK_SHADOW_IN</property>
2871           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2872
2873           <child>
2874             <widget class="GtkTextView" id="TextDialogTextView">
2875               <property name="visible">True</property>
2876               <property name="can_focus">True</property>
2877               <property name="editable">True</property>
2878               <property name="overwrite">False</property>
2879               <property name="accepts_tab">True</property>
2880               <property name="justification">GTK_JUSTIFY_LEFT</property>
2881               <property name="wrap_mode">GTK_WRAP_NONE</property>
2882               <property name="cursor_visible">True</property>
2883               <property name="pixels_above_lines">0</property>
2884               <property name="pixels_below_lines">0</property>
2885               <property name="pixels_inside_wrap">0</property>
2886               <property name="left_margin">0</property>
2887               <property name="right_margin">0</property>
2888               <property name="indent">0</property>
2889               <property name="text" translatable="yes"></property>
2890             </widget>
2891           </child>
2892         </widget>
2893         <packing>
2894           <property name="padding">0</property>
2895           <property name="expand">True</property>
2896           <property name="fill">True</property>
2897         </packing>
2898       </child>
2899     </widget>
2900   </child>
2901 </widget>
2902
2903 <widget class="GtkDialog" id="UriChoiceDialog">
2904   <property name="height_request">280</property>
2905   <property name="title" translatable="yes">Uri choice</property>
2906   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2907   <property name="window_position">GTK_WIN_POS_CENTER</property>
2908   <property name="modal">True</property>
2909   <property name="resizable">True</property>
2910   <property name="destroy_with_parent">False</property>
2911   <property name="decorated">True</property>
2912   <property name="skip_taskbar_hint">False</property>
2913   <property name="skip_pager_hint">False</property>
2914   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2915   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2916   <property name="focus_on_map">True</property>
2917   <property name="urgency_hint">False</property>
2918   <property name="has_separator">True</property>
2919
2920   <child internal-child="vbox">
2921     <widget class="GtkVBox" id="dialog-vbox3">
2922       <property name="visible">True</property>
2923       <property name="homogeneous">False</property>
2924       <property name="spacing">4</property>
2925
2926       <child internal-child="action_area">
2927         <widget class="GtkHButtonBox" id="dialog-action_area3">
2928           <property name="visible">True</property>
2929           <property name="layout_style">GTK_BUTTONBOX_END</property>
2930
2931           <child>
2932             <widget class="GtkButton" id="UriChoiceAbortButton">
2933               <property name="visible">True</property>
2934               <property name="can_default">True</property>
2935               <property name="can_focus">True</property>
2936               <property name="label">gtk-cancel</property>
2937               <property name="use_stock">True</property>
2938               <property name="relief">GTK_RELIEF_NORMAL</property>
2939               <property name="focus_on_click">True</property>
2940               <property name="response_id">-6</property>
2941             </widget>
2942           </child>
2943
2944           <child>
2945             <widget class="GtkButton" id="UriChoiceSelectedButton">
2946               <property name="visible">True</property>
2947               <property name="can_default">True</property>
2948               <property name="can_focus">True</property>
2949               <property name="relief">GTK_RELIEF_NORMAL</property>
2950               <property name="focus_on_click">True</property>
2951               <property name="response_id">0</property>
2952
2953               <child>
2954                 <widget class="GtkAlignment" id="alignment2">
2955                   <property name="visible">True</property>
2956                   <property name="xalign">0.5</property>
2957                   <property name="yalign">0.5</property>
2958                   <property name="xscale">0</property>
2959                   <property name="yscale">0</property>
2960                   <property name="top_padding">0</property>
2961                   <property name="bottom_padding">0</property>
2962                   <property name="left_padding">0</property>
2963                   <property name="right_padding">0</property>
2964
2965                   <child>
2966                     <widget class="GtkHBox" id="hbox3">
2967                       <property name="visible">True</property>
2968                       <property name="homogeneous">False</property>
2969                       <property name="spacing">2</property>
2970
2971                       <child>
2972                         <widget class="GtkImage" id="image19">
2973                           <property name="visible">True</property>
2974                           <property name="stock">gtk-index</property>
2975                           <property name="icon_size">4</property>
2976                           <property name="xalign">0.5</property>
2977                           <property name="yalign">0.5</property>
2978                           <property name="xpad">0</property>
2979                           <property name="ypad">0</property>
2980                         </widget>
2981                         <packing>
2982                           <property name="padding">0</property>
2983                           <property name="expand">False</property>
2984                           <property name="fill">False</property>
2985                         </packing>
2986                       </child>
2987
2988                       <child>
2989                         <widget class="GtkLabel" id="label3">
2990                           <property name="visible">True</property>
2991                           <property name="label" translatable="yes">Try _Selected</property>
2992                           <property name="use_underline">True</property>
2993                           <property name="use_markup">False</property>
2994                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2995                           <property name="wrap">False</property>
2996                           <property name="selectable">False</property>
2997                           <property name="xalign">0.5</property>
2998                           <property name="yalign">0.5</property>
2999                           <property name="xpad">0</property>
3000                           <property name="ypad">0</property>
3001                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3002                           <property name="width_chars">-1</property>
3003                           <property name="single_line_mode">False</property>
3004                           <property name="angle">0</property>
3005                         </widget>
3006                         <packing>
3007                           <property name="padding">0</property>
3008                           <property name="expand">False</property>
3009                           <property name="fill">False</property>
3010                         </packing>
3011                       </child>
3012                     </widget>
3013                   </child>
3014                 </widget>
3015               </child>
3016             </widget>
3017           </child>
3018
3019           <child>
3020             <widget class="GtkButton" id="UriChoiceConstantsButton">
3021               <property name="visible">True</property>
3022               <property name="sensitive">False</property>
3023               <property name="can_default">True</property>
3024               <property name="can_focus">True</property>
3025               <property name="label" translatable="yes">Try Constants</property>
3026               <property name="use_underline">True</property>
3027               <property name="relief">GTK_RELIEF_NORMAL</property>
3028               <property name="focus_on_click">True</property>
3029               <property name="response_id">0</property>
3030             </widget>
3031           </child>
3032
3033           <child>
3034             <widget class="GtkButton" id="copyButton">
3035               <property name="can_default">True</property>
3036               <property name="can_focus">True</property>
3037               <property name="label">gtk-copy</property>
3038               <property name="use_stock">True</property>
3039               <property name="relief">GTK_RELIEF_NORMAL</property>
3040               <property name="focus_on_click">True</property>
3041               <property name="response_id">0</property>
3042             </widget>
3043           </child>
3044
3045           <child>
3046             <widget class="GtkButton" id="uriChoiceAutoButton">
3047               <property name="visible">True</property>
3048               <property name="can_default">True</property>
3049               <property name="can_focus">True</property>
3050               <property name="relief">GTK_RELIEF_NORMAL</property>
3051               <property name="focus_on_click">True</property>
3052               <property name="response_id">0</property>
3053
3054               <child>
3055                 <widget class="GtkAlignment" id="alignment5">
3056                   <property name="visible">True</property>
3057                   <property name="xalign">0.5</property>
3058                   <property name="yalign">0.5</property>
3059                   <property name="xscale">0</property>
3060                   <property name="yscale">0</property>
3061                   <property name="top_padding">0</property>
3062                   <property name="bottom_padding">0</property>
3063                   <property name="left_padding">0</property>
3064                   <property name="right_padding">0</property>
3065
3066                   <child>
3067                     <widget class="GtkHBox" id="hbox16">
3068                       <property name="visible">True</property>
3069                       <property name="homogeneous">False</property>
3070                       <property name="spacing">2</property>
3071
3072                       <child>
3073                         <widget class="GtkImage" id="image302">
3074                           <property name="visible">True</property>
3075                           <property name="stock">gtk-ok</property>
3076                           <property name="icon_size">4</property>
3077                           <property name="xalign">0.5</property>
3078                           <property name="yalign">0.5</property>
3079                           <property name="xpad">0</property>
3080                           <property name="ypad">0</property>
3081                         </widget>
3082                         <packing>
3083                           <property name="padding">0</property>
3084                           <property name="expand">False</property>
3085                           <property name="fill">False</property>
3086                         </packing>
3087                       </child>
3088
3089                       <child>
3090                         <widget class="GtkLabel" id="okLabel">
3091                           <property name="visible">True</property>
3092                           <property name="label" translatable="yes">bla bla bla</property>
3093                           <property name="use_underline">True</property>
3094                           <property name="use_markup">False</property>
3095                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3096                           <property name="wrap">False</property>
3097                           <property name="selectable">False</property>
3098                           <property name="xalign">0.5</property>
3099                           <property name="yalign">0.5</property>
3100                           <property name="xpad">0</property>
3101                           <property name="ypad">0</property>
3102                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3103                           <property name="width_chars">-1</property>
3104                           <property name="single_line_mode">False</property>
3105                           <property name="angle">0</property>
3106                         </widget>
3107                         <packing>
3108                           <property name="padding">0</property>
3109                           <property name="expand">False</property>
3110                           <property name="fill">False</property>
3111                         </packing>
3112                       </child>
3113                     </widget>
3114                   </child>
3115                 </widget>
3116               </child>
3117             </widget>
3118           </child>
3119
3120           <child>
3121             <widget class="GtkButton" id="uriChoiceForwardButton">
3122               <property name="visible">True</property>
3123               <property name="can_default">True</property>
3124               <property name="can_focus">True</property>
3125               <property name="label">gtk-go-forward</property>
3126               <property name="use_stock">True</property>
3127               <property name="relief">GTK_RELIEF_NORMAL</property>
3128               <property name="focus_on_click">True</property>
3129               <property name="response_id">0</property>
3130             </widget>
3131           </child>
3132         </widget>
3133         <packing>
3134           <property name="padding">0</property>
3135           <property name="expand">False</property>
3136           <property name="fill">True</property>
3137           <property name="pack_type">GTK_PACK_END</property>
3138         </packing>
3139       </child>
3140
3141       <child>
3142         <widget class="GtkVBox" id="vbox2">
3143           <property name="visible">True</property>
3144           <property name="homogeneous">False</property>
3145           <property name="spacing">3</property>
3146
3147           <child>
3148             <widget class="GtkLabel" id="UriChoiceLabel">
3149               <property name="visible">True</property>
3150               <property name="label" translatable="yes">some informative message here ...</property>
3151               <property name="use_underline">False</property>
3152               <property name="use_markup">False</property>
3153               <property name="justify">GTK_JUSTIFY_LEFT</property>
3154               <property name="wrap">False</property>
3155               <property name="selectable">False</property>
3156               <property name="xalign">0.5</property>
3157               <property name="yalign">0.5</property>
3158               <property name="xpad">0</property>
3159               <property name="ypad">0</property>
3160               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3161               <property name="width_chars">-1</property>
3162               <property name="single_line_mode">False</property>
3163               <property name="angle">0</property>
3164             </widget>
3165             <packing>
3166               <property name="padding">0</property>
3167               <property name="expand">False</property>
3168               <property name="fill">False</property>
3169             </packing>
3170           </child>
3171
3172           <child>
3173             <widget class="GtkScrolledWindow" id="scrolledwindow1">
3174               <property name="width_request">400</property>
3175               <property name="visible">True</property>
3176               <property name="can_focus">True</property>
3177               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3178               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3179               <property name="shadow_type">GTK_SHADOW_NONE</property>
3180               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3181
3182               <child>
3183                 <widget class="GtkTreeView" id="UriChoiceTreeView">
3184                   <property name="visible">True</property>
3185                   <property name="can_focus">True</property>
3186                   <property name="headers_visible">False</property>
3187                   <property name="rules_hint">False</property>
3188                   <property name="reorderable">False</property>
3189                   <property name="enable_search">True</property>
3190                   <property name="fixed_height_mode">False</property>
3191                   <property name="hover_selection">False</property>
3192                   <property name="hover_expand">False</property>
3193                 </widget>
3194               </child>
3195             </widget>
3196             <packing>
3197               <property name="padding">0</property>
3198               <property name="expand">True</property>
3199               <property name="fill">True</property>
3200             </packing>
3201           </child>
3202
3203           <child>
3204             <widget class="GtkHBox" id="uriEntryHBox">
3205               <property name="visible">True</property>
3206               <property name="homogeneous">False</property>
3207               <property name="spacing">0</property>
3208
3209               <child>
3210                 <widget class="GtkLabel" id="label2">
3211                   <property name="visible">True</property>
3212                   <property name="label" translatable="yes">URI: </property>
3213                   <property name="use_underline">False</property>
3214                   <property name="use_markup">False</property>
3215                   <property name="justify">GTK_JUSTIFY_LEFT</property>
3216                   <property name="wrap">False</property>
3217                   <property name="selectable">False</property>
3218                   <property name="xalign">0.5</property>
3219                   <property name="yalign">0.5</property>
3220                   <property name="xpad">0</property>
3221                   <property name="ypad">0</property>
3222                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3223                   <property name="width_chars">-1</property>
3224                   <property name="single_line_mode">False</property>
3225                   <property name="angle">0</property>
3226                 </widget>
3227                 <packing>
3228                   <property name="padding">0</property>
3229                   <property name="expand">False</property>
3230                   <property name="fill">False</property>
3231                 </packing>
3232               </child>
3233
3234               <child>
3235                 <widget class="GtkEntry" id="entry1">
3236                   <property name="visible">True</property>
3237                   <property name="can_focus">True</property>
3238                   <property name="editable">True</property>
3239                   <property name="visibility">True</property>
3240                   <property name="max_length">0</property>
3241                   <property name="text" translatable="yes"></property>
3242                   <property name="has_frame">True</property>
3243                   <property name="invisible_char">*</property>
3244                   <property name="activates_default">False</property>
3245                 </widget>
3246                 <packing>
3247                   <property name="padding">0</property>
3248                   <property name="expand">True</property>
3249                   <property name="fill">True</property>
3250                 </packing>
3251               </child>
3252             </widget>
3253             <packing>
3254               <property name="padding">0</property>
3255               <property name="expand">False</property>
3256               <property name="fill">True</property>
3257             </packing>
3258           </child>
3259         </widget>
3260         <packing>
3261           <property name="padding">0</property>
3262           <property name="expand">True</property>
3263           <property name="fill">True</property>
3264         </packing>
3265       </child>
3266     </widget>
3267   </child>
3268 </widget>
3269
3270 <widget class="GtkWindow" id="FindReplWin">
3271   <property name="border_width">5</property>
3272   <property name="title" translatable="yes">Find &amp; Replace</property>
3273   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3274   <property name="window_position">GTK_WIN_POS_MOUSE</property>
3275   <property name="modal">False</property>
3276   <property name="resizable">False</property>
3277   <property name="destroy_with_parent">False</property>
3278   <property name="decorated">True</property>
3279   <property name="skip_taskbar_hint">False</property>
3280   <property name="skip_pager_hint">False</property>
3281   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3282   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3283   <property name="focus_on_map">True</property>
3284   <property name="urgency_hint">False</property>
3285
3286   <child>
3287     <widget class="GtkTable" id="table1">
3288       <property name="visible">True</property>
3289       <property name="n_rows">3</property>
3290       <property name="n_columns">2</property>
3291       <property name="homogeneous">False</property>
3292       <property name="row_spacing">5</property>
3293       <property name="column_spacing">0</property>
3294
3295       <child>
3296         <widget class="GtkLabel" id="label17">
3297           <property name="visible">True</property>
3298           <property name="label" translatable="yes">Find:</property>
3299           <property name="use_underline">False</property>
3300           <property name="use_markup">False</property>
3301           <property name="justify">GTK_JUSTIFY_LEFT</property>
3302           <property name="wrap">False</property>
3303           <property name="selectable">False</property>
3304           <property name="xalign">0</property>
3305           <property name="yalign">0.5</property>
3306           <property name="xpad">0</property>
3307           <property name="ypad">0</property>
3308           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3309           <property name="width_chars">-1</property>
3310           <property name="single_line_mode">False</property>
3311           <property name="angle">0</property>
3312         </widget>
3313         <packing>
3314           <property name="left_attach">0</property>
3315           <property name="right_attach">1</property>
3316           <property name="top_attach">0</property>
3317           <property name="bottom_attach">1</property>
3318           <property name="x_options">fill</property>
3319           <property name="y_options"></property>
3320         </packing>
3321       </child>
3322
3323       <child>
3324         <widget class="GtkLabel" id="label18">
3325           <property name="visible">True</property>
3326           <property name="label" translatable="yes">Replace with: </property>
3327           <property name="use_underline">False</property>
3328           <property name="use_markup">False</property>
3329           <property name="justify">GTK_JUSTIFY_LEFT</property>
3330           <property name="wrap">False</property>
3331           <property name="selectable">False</property>
3332           <property name="xalign">0</property>
3333           <property name="yalign">0.5</property>
3334           <property name="xpad">0</property>
3335           <property name="ypad">0</property>
3336           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3337           <property name="width_chars">-1</property>
3338           <property name="single_line_mode">False</property>
3339           <property name="angle">0</property>
3340         </widget>
3341         <packing>
3342           <property name="left_attach">0</property>
3343           <property name="right_attach">1</property>
3344           <property name="top_attach">1</property>
3345           <property name="bottom_attach">2</property>
3346           <property name="x_options">fill</property>
3347           <property name="y_options"></property>
3348         </packing>
3349       </child>
3350
3351       <child>
3352         <widget class="GtkEntry" id="findEntry">
3353           <property name="visible">True</property>
3354           <property name="can_default">True</property>
3355           <property name="has_default">True</property>
3356           <property name="can_focus">True</property>
3357           <property name="has_focus">True</property>
3358           <property name="editable">True</property>
3359           <property name="visibility">True</property>
3360           <property name="max_length">0</property>
3361           <property name="text" translatable="yes"></property>
3362           <property name="has_frame">True</property>
3363           <property name="invisible_char">*</property>
3364           <property name="activates_default">False</property>
3365         </widget>
3366         <packing>
3367           <property name="left_attach">1</property>
3368           <property name="right_attach">2</property>
3369           <property name="top_attach">0</property>
3370           <property name="bottom_attach">1</property>
3371           <property name="y_options"></property>
3372         </packing>
3373       </child>
3374
3375       <child>
3376         <widget class="GtkEntry" id="replaceEntry">
3377           <property name="visible">True</property>
3378           <property name="can_focus">True</property>
3379           <property name="editable">True</property>
3380           <property name="visibility">True</property>
3381           <property name="max_length">0</property>
3382           <property name="text" translatable="yes"></property>
3383           <property name="has_frame">True</property>
3384           <property name="invisible_char">*</property>
3385           <property name="activates_default">False</property>
3386         </widget>
3387         <packing>
3388           <property name="left_attach">1</property>
3389           <property name="right_attach">2</property>
3390           <property name="top_attach">1</property>
3391           <property name="bottom_attach">2</property>
3392           <property name="y_options"></property>
3393         </packing>
3394       </child>
3395
3396       <child>
3397         <widget class="GtkHBox" id="hbox19">
3398           <property name="visible">True</property>
3399           <property name="homogeneous">False</property>
3400           <property name="spacing">5</property>
3401
3402           <child>
3403             <widget class="GtkVBox" id="vbox9">
3404               <property name="visible">True</property>
3405               <property name="homogeneous">False</property>
3406               <property name="spacing">0</property>
3407
3408               <child>
3409                 <placeholder/>
3410               </child>
3411
3412               <child>
3413                 <placeholder/>
3414               </child>
3415             </widget>
3416             <packing>
3417               <property name="padding">0</property>
3418               <property name="expand">True</property>
3419               <property name="fill">True</property>
3420             </packing>
3421           </child>
3422
3423           <child>
3424             <widget class="GtkButton" id="findButton">
3425               <property name="visible">True</property>
3426               <property name="can_focus">True</property>
3427               <property name="label">gtk-find</property>
3428               <property name="use_stock">True</property>
3429               <property name="relief">GTK_RELIEF_NORMAL</property>
3430               <property name="focus_on_click">True</property>
3431             </widget>
3432             <packing>
3433               <property name="padding">0</property>
3434               <property name="expand">False</property>
3435               <property name="fill">False</property>
3436             </packing>
3437           </child>
3438
3439           <child>
3440             <widget class="GtkButton" id="findReplButton">
3441               <property name="visible">True</property>
3442               <property name="can_focus">True</property>
3443               <property name="relief">GTK_RELIEF_NORMAL</property>
3444               <property name="focus_on_click">True</property>
3445
3446               <child>
3447                 <widget class="GtkAlignment" id="alignment13">
3448                   <property name="visible">True</property>
3449                   <property name="xalign">0.5</property>
3450                   <property name="yalign">0.5</property>
3451                   <property name="xscale">0</property>
3452                   <property name="yscale">0</property>
3453                   <property name="top_padding">0</property>
3454                   <property name="bottom_padding">0</property>
3455                   <property name="left_padding">0</property>
3456                   <property name="right_padding">0</property>
3457
3458                   <child>
3459                     <widget class="GtkHBox" id="hbox20">
3460                       <property name="visible">True</property>
3461                       <property name="homogeneous">False</property>
3462                       <property name="spacing">2</property>
3463
3464                       <child>
3465                         <widget class="GtkImage" id="image357">
3466                           <property name="visible">True</property>
3467                           <property name="stock">gtk-find-and-replace</property>
3468                           <property name="icon_size">4</property>
3469                           <property name="xalign">0.5</property>
3470                           <property name="yalign">0.5</property>
3471                           <property name="xpad">0</property>
3472                           <property name="ypad">0</property>
3473                         </widget>
3474                         <packing>
3475                           <property name="padding">0</property>
3476                           <property name="expand">False</property>
3477                           <property name="fill">False</property>
3478                         </packing>
3479                       </child>
3480
3481                       <child>
3482                         <widget class="GtkLabel" id="label19">
3483                           <property name="visible">True</property>
3484                           <property name="label">_Replace</property>
3485                           <property name="use_underline">True</property>
3486                           <property name="use_markup">False</property>
3487                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3488                           <property name="wrap">False</property>
3489                           <property name="selectable">False</property>
3490                           <property name="xalign">0.5</property>
3491                           <property name="yalign">0.5</property>
3492                           <property name="xpad">0</property>
3493                           <property name="ypad">0</property>
3494                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3495                           <property name="width_chars">-1</property>
3496                           <property name="single_line_mode">False</property>
3497                           <property name="angle">0</property>
3498                         </widget>
3499                         <packing>
3500                           <property name="padding">0</property>
3501                           <property name="expand">False</property>
3502                           <property name="fill">False</property>
3503                         </packing>
3504                       </child>
3505                     </widget>
3506                   </child>
3507                 </widget>
3508               </child>
3509             </widget>
3510             <packing>
3511               <property name="padding">0</property>
3512               <property name="expand">False</property>
3513               <property name="fill">False</property>
3514             </packing>
3515           </child>
3516
3517           <child>
3518             <widget class="GtkButton" id="cancelButton">
3519               <property name="visible">True</property>
3520               <property name="can_focus">True</property>
3521               <property name="label">gtk-cancel</property>
3522               <property name="use_stock">True</property>
3523               <property name="relief">GTK_RELIEF_NORMAL</property>
3524               <property name="focus_on_click">True</property>
3525             </widget>
3526             <packing>
3527               <property name="padding">0</property>
3528               <property name="expand">False</property>
3529               <property name="fill">False</property>
3530             </packing>
3531           </child>
3532         </widget>
3533         <packing>
3534           <property name="left_attach">0</property>
3535           <property name="right_attach">2</property>
3536           <property name="top_attach">2</property>
3537           <property name="bottom_attach">3</property>
3538           <property name="y_padding">5</property>
3539         </packing>
3540       </child>
3541     </widget>
3542   </child>
3543 </widget>
3544
3545 <widget class="GtkWindow" id="NewDevelWin">
3546   <property name="title" translatable="yes">Create development</property>
3547   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3548   <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
3549   <property name="modal">True</property>
3550   <property name="resizable">False</property>
3551   <property name="destroy_with_parent">False</property>
3552   <property name="decorated">True</property>
3553   <property name="skip_taskbar_hint">False</property>
3554   <property name="skip_pager_hint">False</property>
3555   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
3556   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3557   <property name="focus_on_map">True</property>
3558   <property name="urgency_hint">False</property>
3559
3560   <child>
3561     <widget class="GtkVBox" id="vbox10">
3562       <property name="visible">True</property>
3563       <property name="homogeneous">False</property>
3564       <property name="spacing">0</property>
3565
3566       <child>
3567         <widget class="GtkTable" id="table2">
3568           <property name="border_width">3</property>
3569           <property name="visible">True</property>
3570           <property name="n_rows">2</property>
3571           <property name="n_columns">3</property>
3572           <property name="homogeneous">False</property>
3573           <property name="row_spacing">5</property>
3574           <property name="column_spacing">5</property>
3575
3576           <child>
3577             <widget class="GtkLabel" id="label20">
3578               <property name="visible">True</property>
3579               <property name="label" translatable="yes">Name</property>
3580               <property name="use_underline">False</property>
3581               <property name="use_markup">False</property>
3582               <property name="justify">GTK_JUSTIFY_LEFT</property>
3583               <property name="wrap">False</property>
3584               <property name="selectable">False</property>
3585               <property name="xalign">0</property>
3586               <property name="yalign">0.5</property>
3587               <property name="xpad">0</property>
3588               <property name="ypad">0</property>
3589               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3590               <property name="width_chars">-1</property>
3591               <property name="single_line_mode">False</property>
3592               <property name="angle">0</property>
3593             </widget>
3594             <packing>
3595               <property name="left_attach">0</property>
3596               <property name="right_attach">1</property>
3597               <property name="top_attach">0</property>
3598               <property name="bottom_attach">1</property>
3599               <property name="x_options">fill</property>
3600               <property name="y_options"></property>
3601             </packing>
3602           </child>
3603
3604           <child>
3605             <widget class="GtkLabel" id="label21">
3606               <property name="visible">True</property>
3607               <property name="label" translatable="yes">Root directory</property>
3608               <property name="use_underline">False</property>
3609               <property name="use_markup">False</property>
3610               <property name="justify">GTK_JUSTIFY_LEFT</property>
3611               <property name="wrap">False</property>
3612               <property name="selectable">False</property>
3613               <property name="xalign">0</property>
3614               <property name="yalign">0.5</property>
3615               <property name="xpad">0</property>
3616               <property name="ypad">0</property>
3617               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3618               <property name="width_chars">-1</property>
3619               <property name="single_line_mode">False</property>
3620               <property name="angle">0</property>
3621             </widget>
3622             <packing>
3623               <property name="left_attach">0</property>
3624               <property name="right_attach">1</property>
3625               <property name="top_attach">1</property>
3626               <property name="bottom_attach">2</property>
3627               <property name="x_options">fill</property>
3628               <property name="y_options"></property>
3629             </packing>
3630           </child>
3631
3632           <child>
3633             <widget class="GtkEntry" id="nameEntry">
3634               <property name="visible">True</property>
3635               <property name="can_focus">True</property>
3636               <property name="editable">True</property>
3637               <property name="visibility">True</property>
3638               <property name="max_length">0</property>
3639               <property name="text" translatable="yes"></property>
3640               <property name="has_frame">True</property>
3641               <property name="invisible_char">*</property>
3642               <property name="activates_default">False</property>
3643             </widget>
3644             <packing>
3645               <property name="left_attach">1</property>
3646               <property name="right_attach">2</property>
3647               <property name="top_attach">0</property>
3648               <property name="bottom_attach">1</property>
3649               <property name="y_options"></property>
3650             </packing>
3651           </child>
3652
3653           <child>
3654             <widget class="GtkEntry" id="rootEntry">
3655               <property name="visible">True</property>
3656               <property name="can_focus">True</property>
3657               <property name="editable">True</property>
3658               <property name="visibility">True</property>
3659               <property name="max_length">0</property>
3660               <property name="text" translatable="yes"></property>
3661               <property name="has_frame">True</property>
3662               <property name="invisible_char">*</property>
3663               <property name="activates_default">False</property>
3664             </widget>
3665             <packing>
3666               <property name="left_attach">1</property>
3667               <property name="right_attach">2</property>
3668               <property name="top_attach">1</property>
3669               <property name="bottom_attach">2</property>
3670               <property name="y_options"></property>
3671             </packing>
3672           </child>
3673
3674           <child>
3675             <widget class="GtkButton" id="chooseRootButton">
3676               <property name="visible">True</property>
3677               <property name="can_focus">True</property>
3678               <property name="label" translatable="yes">...</property>
3679               <property name="use_underline">True</property>
3680               <property name="relief">GTK_RELIEF_NORMAL</property>
3681               <property name="focus_on_click">True</property>
3682             </widget>
3683             <packing>
3684               <property name="left_attach">2</property>
3685               <property name="right_attach">3</property>
3686               <property name="top_attach">1</property>
3687               <property name="bottom_attach">2</property>
3688               <property name="x_options">fill</property>
3689               <property name="y_options"></property>
3690             </packing>
3691           </child>
3692         </widget>
3693         <packing>
3694           <property name="padding">0</property>
3695           <property name="expand">False</property>
3696           <property name="fill">True</property>
3697         </packing>
3698       </child>
3699
3700       <child>
3701         <widget class="GtkHSeparator" id="hseparator1">
3702           <property name="visible">True</property>
3703         </widget>
3704         <packing>
3705           <property name="padding">2</property>
3706           <property name="expand">False</property>
3707           <property name="fill">True</property>
3708         </packing>
3709       </child>
3710
3711       <child>
3712         <widget class="GtkHBox" id="hbox21">
3713           <property name="border_width">3</property>
3714           <property name="visible">True</property>
3715           <property name="homogeneous">False</property>
3716           <property name="spacing">5</property>
3717
3718           <child>
3719             <widget class="GtkVBox" id="vbox11">
3720               <property name="visible">True</property>
3721               <property name="homogeneous">False</property>
3722               <property name="spacing">0</property>
3723
3724               <child>
3725                 <placeholder/>
3726               </child>
3727
3728               <child>
3729                 <placeholder/>
3730               </child>
3731             </widget>
3732             <packing>
3733               <property name="padding">0</property>
3734               <property name="expand">True</property>
3735               <property name="fill">True</property>
3736             </packing>
3737           </child>
3738
3739           <child>
3740             <widget class="GtkButton" id="addButton">
3741               <property name="visible">True</property>
3742               <property name="can_focus">True</property>
3743               <property name="label">gtk-add</property>
3744               <property name="use_stock">True</property>
3745               <property name="relief">GTK_RELIEF_NORMAL</property>
3746               <property name="focus_on_click">True</property>
3747             </widget>
3748             <packing>
3749               <property name="padding">0</property>
3750               <property name="expand">False</property>
3751               <property name="fill">False</property>
3752             </packing>
3753           </child>
3754
3755           <child>
3756             <widget class="GtkButton" id="cancelButton">
3757               <property name="visible">True</property>
3758               <property name="can_focus">True</property>
3759               <property name="label">gtk-cancel</property>
3760               <property name="use_stock">True</property>
3761               <property name="relief">GTK_RELIEF_NORMAL</property>
3762               <property name="focus_on_click">True</property>
3763             </widget>
3764             <packing>
3765               <property name="padding">0</property>
3766               <property name="expand">False</property>
3767               <property name="fill">False</property>
3768             </packing>
3769           </child>
3770         </widget>
3771         <packing>
3772           <property name="padding">0</property>
3773           <property name="expand">False</property>
3774           <property name="fill">True</property>
3775         </packing>
3776       </child>
3777     </widget>
3778   </child>
3779 </widget>
3780
3781 <widget class="GtkWindow" id="DevelListWin">
3782   <property name="title" translatable="yes">Developments</property>
3783   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3784   <property name="window_position">GTK_WIN_POS_CENTER</property>
3785   <property name="modal">False</property>
3786   <property name="resizable">True</property>
3787   <property name="destroy_with_parent">False</property>
3788   <property name="decorated">True</property>
3789   <property name="skip_taskbar_hint">False</property>
3790   <property name="skip_pager_hint">False</property>
3791   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
3792   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3793   <property name="focus_on_map">True</property>
3794   <property name="urgency_hint">False</property>
3795
3796   <child>
3797     <widget class="GtkVBox" id="vbox12">
3798       <property name="visible">True</property>
3799       <property name="homogeneous">False</property>
3800       <property name="spacing">0</property>
3801
3802       <child>
3803         <widget class="GtkScrolledWindow" id="scrolledwindow10">
3804           <property name="visible">True</property>
3805           <property name="can_focus">True</property>
3806           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3807           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3808           <property name="shadow_type">GTK_SHADOW_IN</property>
3809           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3810
3811           <child>
3812             <widget class="GtkTreeView" id="developmentsTreeview">
3813               <property name="visible">True</property>
3814               <property name="can_focus">True</property>
3815               <property name="headers_visible">False</property>
3816               <property name="rules_hint">False</property>
3817               <property name="reorderable">False</property>
3818               <property name="enable_search">True</property>
3819               <property name="fixed_height_mode">False</property>
3820               <property name="hover_selection">False</property>
3821               <property name="hover_expand">False</property>
3822             </widget>
3823           </child>
3824         </widget>
3825         <packing>
3826           <property name="padding">0</property>
3827           <property name="expand">True</property>
3828           <property name="fill">True</property>
3829         </packing>
3830       </child>
3831
3832       <child>
3833         <widget class="GtkHSeparator" id="hseparator2">
3834           <property name="visible">True</property>
3835         </widget>
3836         <packing>
3837           <property name="padding">2</property>
3838           <property name="expand">False</property>
3839           <property name="fill">True</property>
3840         </packing>
3841       </child>
3842
3843       <child>
3844         <widget class="GtkHBox" id="buttonsHbox">
3845           <property name="border_width">3</property>
3846           <property name="visible">True</property>
3847           <property name="homogeneous">False</property>
3848           <property name="spacing">4</property>
3849
3850           <child>
3851             <widget class="GtkVBox" id="vbox13">
3852               <property name="visible">True</property>
3853               <property name="homogeneous">False</property>
3854               <property name="spacing">0</property>
3855
3856               <child>
3857                 <placeholder/>
3858               </child>
3859
3860               <child>
3861                 <placeholder/>
3862               </child>
3863             </widget>
3864             <packing>
3865               <property name="padding">0</property>
3866               <property name="expand">True</property>
3867               <property name="fill">True</property>
3868             </packing>
3869           </child>
3870
3871           <child>
3872             <widget class="GtkButton" id="newButton">
3873               <property name="visible">True</property>
3874               <property name="can_focus">True</property>
3875               <property name="label">gtk-new</property>
3876               <property name="use_stock">True</property>
3877               <property name="relief">GTK_RELIEF_NORMAL</property>
3878               <property name="focus_on_click">True</property>
3879             </widget>
3880             <packing>
3881               <property name="padding">0</property>
3882               <property name="expand">False</property>
3883               <property name="fill">False</property>
3884             </packing>
3885           </child>
3886
3887           <child>
3888             <widget class="GtkButton" id="deleteButton">
3889               <property name="visible">True</property>
3890               <property name="can_focus">True</property>
3891               <property name="label">gtk-delete</property>
3892               <property name="use_stock">True</property>
3893               <property name="relief">GTK_RELIEF_NORMAL</property>
3894               <property name="focus_on_click">True</property>
3895             </widget>
3896             <packing>
3897               <property name="padding">0</property>
3898               <property name="expand">False</property>
3899               <property name="fill">False</property>
3900             </packing>
3901           </child>
3902
3903           <child>
3904             <widget class="GtkButton" id="buildButton">
3905               <property name="visible">True</property>
3906               <property name="can_focus">True</property>
3907               <property name="relief">GTK_RELIEF_NORMAL</property>
3908               <property name="focus_on_click">True</property>
3909
3910               <child>
3911                 <widget class="GtkAlignment" id="alignment14">
3912                   <property name="visible">True</property>
3913                   <property name="xalign">0.5</property>
3914                   <property name="yalign">0.5</property>
3915                   <property name="xscale">0</property>
3916                   <property name="yscale">0</property>
3917                   <property name="top_padding">0</property>
3918                   <property name="bottom_padding">0</property>
3919                   <property name="left_padding">0</property>
3920                   <property name="right_padding">0</property>
3921
3922                   <child>
3923                     <widget class="GtkHBox" id="hbox23">
3924                       <property name="visible">True</property>
3925                       <property name="homogeneous">False</property>
3926                       <property name="spacing">2</property>
3927
3928                       <child>
3929                         <widget class="GtkImage" id="image358">
3930                           <property name="visible">True</property>
3931                           <property name="stock">gtk-execute</property>
3932                           <property name="icon_size">4</property>
3933                           <property name="xalign">0.5</property>
3934                           <property name="yalign">0.5</property>
3935                           <property name="xpad">0</property>
3936                           <property name="ypad">0</property>
3937                         </widget>
3938                         <packing>
3939                           <property name="padding">0</property>
3940                           <property name="expand">False</property>
3941                           <property name="fill">False</property>
3942                         </packing>
3943                       </child>
3944
3945                       <child>
3946                         <widget class="GtkLabel" id="label22">
3947                           <property name="visible">True</property>
3948                           <property name="label" translatable="yes">_Build</property>
3949                           <property name="use_underline">True</property>
3950                           <property name="use_markup">False</property>
3951                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3952                           <property name="wrap">False</property>
3953                           <property name="selectable">False</property>
3954                           <property name="xalign">0.5</property>
3955                           <property name="yalign">0.5</property>
3956                           <property name="xpad">0</property>
3957                           <property name="ypad">0</property>
3958                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3959                           <property name="width_chars">-1</property>
3960                           <property name="single_line_mode">False</property>
3961                           <property name="angle">0</property>
3962                         </widget>
3963                         <packing>
3964                           <property name="padding">0</property>
3965                           <property name="expand">False</property>
3966                           <property name="fill">False</property>
3967                         </packing>
3968                       </child>
3969                     </widget>
3970                   </child>
3971                 </widget>
3972               </child>
3973             </widget>
3974             <packing>
3975               <property name="padding">0</property>
3976               <property name="expand">False</property>
3977               <property name="fill">False</property>
3978             </packing>
3979           </child>
3980
3981           <child>
3982             <widget class="GtkButton" id="cleanButton">
3983               <property name="visible">True</property>
3984               <property name="can_focus">True</property>
3985               <property name="relief">GTK_RELIEF_NORMAL</property>
3986               <property name="focus_on_click">True</property>
3987
3988               <child>
3989                 <widget class="GtkAlignment" id="alignment15">
3990                   <property name="visible">True</property>
3991                   <property name="xalign">0.5</property>
3992                   <property name="yalign">0.5</property>
3993                   <property name="xscale">0</property>
3994                   <property name="yscale">0</property>
3995                   <property name="top_padding">0</property>
3996                   <property name="bottom_padding">0</property>
3997                   <property name="left_padding">0</property>
3998                   <property name="right_padding">0</property>
3999
4000                   <child>
4001                     <widget class="GtkHBox" id="hbox24">
4002                       <property name="visible">True</property>
4003                       <property name="homogeneous">False</property>
4004                       <property name="spacing">2</property>
4005
4006                       <child>
4007                         <widget class="GtkImage" id="image359">
4008                           <property name="visible">True</property>
4009                           <property name="stock">gtk-clear</property>
4010                           <property name="icon_size">4</property>
4011                           <property name="xalign">0.5</property>
4012                           <property name="yalign">0.5</property>
4013                           <property name="xpad">0</property>
4014                           <property name="ypad">0</property>
4015                         </widget>
4016                         <packing>
4017                           <property name="padding">0</property>
4018                           <property name="expand">False</property>
4019                           <property name="fill">False</property>
4020                         </packing>
4021                       </child>
4022
4023                       <child>
4024                         <widget class="GtkLabel" id="label23">
4025                           <property name="visible">True</property>
4026                           <property name="label" translatable="yes">C_lean</property>
4027                           <property name="use_underline">True</property>
4028                           <property name="use_markup">False</property>
4029                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4030                           <property name="wrap">False</property>
4031                           <property name="selectable">False</property>
4032                           <property name="xalign">0.5</property>
4033                           <property name="yalign">0.5</property>
4034                           <property name="xpad">0</property>
4035                           <property name="ypad">0</property>
4036                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4037                           <property name="width_chars">-1</property>
4038                           <property name="single_line_mode">False</property>
4039                           <property name="angle">0</property>
4040                         </widget>
4041                         <packing>
4042                           <property name="padding">0</property>
4043                           <property name="expand">False</property>
4044                           <property name="fill">False</property>
4045                         </packing>
4046                       </child>
4047                     </widget>
4048                   </child>
4049                 </widget>
4050               </child>
4051             </widget>
4052             <packing>
4053               <property name="padding">0</property>
4054               <property name="expand">False</property>
4055               <property name="fill">False</property>
4056             </packing>
4057           </child>
4058
4059           <child>
4060             <widget class="GtkButton" id="publishButton">
4061               <property name="visible">True</property>
4062               <property name="can_focus">True</property>
4063               <property name="relief">GTK_RELIEF_NORMAL</property>
4064               <property name="focus_on_click">True</property>
4065
4066               <child>
4067                 <widget class="GtkAlignment" id="alignment16">
4068                   <property name="visible">True</property>
4069                   <property name="xalign">0.5</property>
4070                   <property name="yalign">0.5</property>
4071                   <property name="xscale">0</property>
4072                   <property name="yscale">0</property>
4073                   <property name="top_padding">0</property>
4074                   <property name="bottom_padding">0</property>
4075                   <property name="left_padding">0</property>
4076                   <property name="right_padding">0</property>
4077
4078                   <child>
4079                     <widget class="GtkHBox" id="hbox25">
4080                       <property name="visible">True</property>
4081                       <property name="homogeneous">False</property>
4082                       <property name="spacing">2</property>
4083
4084                       <child>
4085                         <widget class="GtkImage" id="image907">
4086                           <property name="visible">True</property>
4087                           <property name="stock">gtk-convert</property>
4088                           <property name="icon_size">4</property>
4089                           <property name="xalign">0.5</property>
4090                           <property name="yalign">0.5</property>
4091                           <property name="xpad">0</property>
4092                           <property name="ypad">0</property>
4093                         </widget>
4094                         <packing>
4095                           <property name="padding">0</property>
4096                           <property name="expand">False</property>
4097                           <property name="fill">False</property>
4098                         </packing>
4099                       </child>
4100
4101                       <child>
4102                         <widget class="GtkLabel" id="label24">
4103                           <property name="visible">True</property>
4104                           <property name="label" translatable="yes">Publish</property>
4105                           <property name="use_underline">True</property>
4106                           <property name="use_markup">False</property>
4107                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4108                           <property name="wrap">False</property>
4109                           <property name="selectable">False</property>
4110                           <property name="xalign">0.5</property>
4111                           <property name="yalign">0.5</property>
4112                           <property name="xpad">0</property>
4113                           <property name="ypad">0</property>
4114                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4115                           <property name="width_chars">-1</property>
4116                           <property name="single_line_mode">False</property>
4117                           <property name="angle">0</property>
4118                         </widget>
4119                         <packing>
4120                           <property name="padding">0</property>
4121                           <property name="expand">False</property>
4122                           <property name="fill">False</property>
4123                         </packing>
4124                       </child>
4125                     </widget>
4126                   </child>
4127                 </widget>
4128               </child>
4129             </widget>
4130             <packing>
4131               <property name="padding">0</property>
4132               <property name="expand">False</property>
4133               <property name="fill">False</property>
4134             </packing>
4135           </child>
4136
4137           <child>
4138             <widget class="GtkButton" id="graphButton">
4139               <property name="visible">True</property>
4140               <property name="can_focus">True</property>
4141               <property name="relief">GTK_RELIEF_NORMAL</property>
4142               <property name="focus_on_click">True</property>
4143
4144               <child>
4145                 <widget class="GtkAlignment" id="alignment17">
4146                   <property name="visible">True</property>
4147                   <property name="xalign">0.5</property>
4148                   <property name="yalign">0.5</property>
4149                   <property name="xscale">0</property>
4150                   <property name="yscale">0</property>
4151                   <property name="top_padding">0</property>
4152                   <property name="bottom_padding">0</property>
4153                   <property name="left_padding">0</property>
4154                   <property name="right_padding">0</property>
4155
4156                   <child>
4157                     <widget class="GtkHBox" id="hbox26">
4158                       <property name="visible">True</property>
4159                       <property name="homogeneous">False</property>
4160                       <property name="spacing">2</property>
4161
4162                       <child>
4163                         <widget class="GtkImage" id="image908">
4164                           <property name="visible">True</property>
4165                           <property name="stock">gtk-zoom-fit</property>
4166                           <property name="icon_size">4</property>
4167                           <property name="xalign">0.5</property>
4168                           <property name="yalign">0.5</property>
4169                           <property name="xpad">0</property>
4170                           <property name="ypad">0</property>
4171                         </widget>
4172                         <packing>
4173                           <property name="padding">0</property>
4174                           <property name="expand">False</property>
4175                           <property name="fill">False</property>
4176                         </packing>
4177                       </child>
4178
4179                       <child>
4180                         <widget class="GtkLabel" id="label27">
4181                           <property name="visible">True</property>
4182                           <property name="label" translatable="yes">Graph</property>
4183                           <property name="use_underline">True</property>
4184                           <property name="use_markup">False</property>
4185                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4186                           <property name="wrap">False</property>
4187                           <property name="selectable">False</property>
4188                           <property name="xalign">0.5</property>
4189                           <property name="yalign">0.5</property>
4190                           <property name="xpad">0</property>
4191                           <property name="ypad">0</property>
4192                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4193                           <property name="width_chars">-1</property>
4194                           <property name="single_line_mode">False</property>
4195                           <property name="angle">0</property>
4196                         </widget>
4197                         <packing>
4198                           <property name="padding">0</property>
4199                           <property name="expand">False</property>
4200                           <property name="fill">False</property>
4201                         </packing>
4202                       </child>
4203                     </widget>
4204                   </child>
4205                 </widget>
4206               </child>
4207             </widget>
4208             <packing>
4209               <property name="padding">0</property>
4210               <property name="expand">False</property>
4211               <property name="fill">False</property>
4212             </packing>
4213           </child>
4214
4215           <child>
4216             <widget class="GtkButton" id="closeButton">
4217               <property name="visible">True</property>
4218               <property name="can_focus">True</property>
4219               <property name="label">gtk-close</property>
4220               <property name="use_stock">True</property>
4221               <property name="relief">GTK_RELIEF_NORMAL</property>
4222               <property name="focus_on_click">True</property>
4223             </widget>
4224             <packing>
4225               <property name="padding">0</property>
4226               <property name="expand">False</property>
4227               <property name="fill">False</property>
4228             </packing>
4229           </child>
4230         </widget>
4231         <packing>
4232           <property name="padding">0</property>
4233           <property name="expand">False</property>
4234           <property name="fill">True</property>
4235         </packing>
4236       </child>
4237     </widget>
4238   </child>
4239 </widget>
4240
4241 <widget class="GtkWindow" id="window1">
4242   <property name="visible">True</property>
4243   <property name="title" translatable="yes">window1</property>
4244   <property name="type">GTK_WINDOW_TOPLEVEL</property>
4245   <property name="window_position">GTK_WIN_POS_NONE</property>
4246   <property name="modal">False</property>
4247   <property name="resizable">True</property>
4248   <property name="destroy_with_parent">False</property>
4249   <property name="decorated">True</property>
4250   <property name="skip_taskbar_hint">False</property>
4251   <property name="skip_pager_hint">False</property>
4252   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
4253   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
4254   <property name="focus_on_map">True</property>
4255   <property name="urgency_hint">False</property>
4256
4257   <child>
4258     <widget class="GtkHBox" id="hbox27">
4259       <property name="visible">True</property>
4260       <property name="homogeneous">False</property>
4261       <property name="spacing">0</property>
4262
4263       <child>
4264         <widget class="GtkToolbar" id="toolbar1">
4265           <property name="visible">True</property>
4266           <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
4267           <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
4268           <property name="tooltips">True</property>
4269           <property name="show_arrow">True</property>
4270
4271           <child>
4272             <widget class="GtkToolItem" id="toolitem30">
4273               <property name="visible">True</property>
4274               <property name="visible_horizontal">True</property>
4275               <property name="visible_vertical">True</property>
4276               <property name="is_important">False</property>
4277
4278               <child>
4279                 <widget class="GtkButton" id="button1">
4280                   <property name="visible">True</property>
4281                   <property name="tooltip" translatable="yes">Restart</property>
4282                   <property name="can_focus">True</property>
4283                   <property name="relief">GTK_RELIEF_NONE</property>
4284                   <property name="focus_on_click">True</property>
4285
4286                   <child>
4287                     <widget class="GtkImage" id="image909">
4288                       <property name="visible">True</property>
4289                       <property name="stock">gtk-goto-top</property>
4290                       <property name="icon_size">4</property>
4291                       <property name="xalign">0.5</property>
4292                       <property name="yalign">0.5</property>
4293                       <property name="xpad">0</property>
4294                       <property name="ypad">0</property>
4295                     </widget>
4296                   </child>
4297                 </widget>
4298               </child>
4299             </widget>
4300             <packing>
4301               <property name="expand">False</property>
4302               <property name="homogeneous">False</property>
4303             </packing>
4304           </child>
4305
4306           <child>
4307             <widget class="GtkToolItem" id="toolitem31">
4308               <property name="visible">True</property>
4309               <property name="visible_horizontal">True</property>
4310               <property name="visible_vertical">True</property>
4311               <property name="is_important">False</property>
4312
4313               <child>
4314                 <widget class="GtkButton" id="button2">
4315                   <property name="visible">True</property>
4316                   <property name="tooltip" translatable="yes">Retract 1 phrase</property>
4317                   <property name="can_focus">True</property>
4318                   <property name="relief">GTK_RELIEF_NONE</property>
4319                   <property name="focus_on_click">True</property>
4320
4321                   <child>
4322                     <widget class="GtkImage" id="image910">
4323                       <property name="visible">True</property>
4324                       <property name="stock">gtk-go-up</property>
4325                       <property name="icon_size">4</property>
4326                       <property name="xalign">0.5</property>
4327                       <property name="yalign">0.5</property>
4328                       <property name="xpad">0</property>
4329                       <property name="ypad">0</property>
4330                     </widget>
4331                   </child>
4332                 </widget>
4333               </child>
4334             </widget>
4335             <packing>
4336               <property name="expand">False</property>
4337               <property name="homogeneous">False</property>
4338             </packing>
4339           </child>
4340
4341           <child>
4342             <widget class="GtkToolItem" id="toolitem32">
4343               <property name="visible">True</property>
4344               <property name="visible_horizontal">True</property>
4345               <property name="visible_vertical">True</property>
4346               <property name="is_important">False</property>
4347
4348               <child>
4349                 <widget class="GtkButton" id="button3">
4350                   <property name="visible">True</property>
4351                   <property name="tooltip" translatable="yes">Execute until point</property>
4352                   <property name="can_focus">True</property>
4353                   <property name="relief">GTK_RELIEF_NONE</property>
4354                   <property name="focus_on_click">True</property>
4355
4356                   <child>
4357                     <widget class="GtkImage" id="image911">
4358                       <property name="visible">True</property>
4359                       <property name="stock">gtk-jump-to</property>
4360                       <property name="icon_size">4</property>
4361                       <property name="xalign">0.5</property>
4362                       <property name="yalign">0.5</property>
4363                       <property name="xpad">0</property>
4364                       <property name="ypad">0</property>
4365                     </widget>
4366                   </child>
4367                 </widget>
4368               </child>
4369             </widget>
4370             <packing>
4371               <property name="expand">False</property>
4372               <property name="homogeneous">False</property>
4373             </packing>
4374           </child>
4375
4376           <child>
4377             <widget class="GtkToolItem" id="toolitem33">
4378               <property name="visible">True</property>
4379               <property name="visible_horizontal">True</property>
4380               <property name="visible_vertical">True</property>
4381               <property name="is_important">False</property>
4382
4383               <child>
4384                 <widget class="GtkButton" id="button4">
4385                   <property name="visible">True</property>
4386                   <property name="tooltip" translatable="yes">Execute 1 phrase</property>
4387                   <property name="can_focus">True</property>
4388                   <property name="relief">GTK_RELIEF_NONE</property>
4389                   <property name="focus_on_click">True</property>
4390
4391                   <child>
4392                     <widget class="GtkImage" id="image912">
4393                       <property name="visible">True</property>
4394                       <property name="stock">gtk-go-down</property>
4395                       <property name="icon_size">4</property>
4396                       <property name="xalign">0.5</property>
4397                       <property name="yalign">0.5</property>
4398                       <property name="xpad">0</property>
4399                       <property name="ypad">0</property>
4400                     </widget>
4401                   </child>
4402                 </widget>
4403               </child>
4404             </widget>
4405             <packing>
4406               <property name="expand">False</property>
4407               <property name="homogeneous">False</property>
4408             </packing>
4409           </child>
4410
4411           <child>
4412             <widget class="GtkToolItem" id="toolitem34">
4413               <property name="visible">True</property>
4414               <property name="visible_horizontal">True</property>
4415               <property name="visible_vertical">True</property>
4416               <property name="is_important">False</property>
4417
4418               <child>
4419                 <widget class="GtkButton" id="button5">
4420                   <property name="visible">True</property>
4421                   <property name="tooltip" translatable="yes">Execute all</property>
4422                   <property name="can_focus">True</property>
4423                   <property name="relief">GTK_RELIEF_NONE</property>
4424                   <property name="focus_on_click">True</property>
4425
4426                   <child>
4427                     <widget class="GtkImage" id="image913">
4428                       <property name="visible">True</property>
4429                       <property name="stock">gtk-goto-bottom</property>
4430                       <property name="icon_size">4</property>
4431                       <property name="xalign">0.5</property>
4432                       <property name="yalign">0.5</property>
4433                       <property name="xpad">0</property>
4434                       <property name="ypad">0</property>
4435                     </widget>
4436                   </child>
4437                 </widget>
4438               </child>
4439             </widget>
4440             <packing>
4441               <property name="expand">False</property>
4442               <property name="homogeneous">False</property>
4443             </packing>
4444           </child>
4445         </widget>
4446         <packing>
4447           <property name="padding">0</property>
4448           <property name="expand">True</property>
4449           <property name="fill">True</property>
4450         </packing>
4451       </child>
4452
4453       <child>
4454         <widget class="GtkImage" id="image914">
4455           <property name="visible">True</property>
4456           <property name="stock">gtk-cancel</property>
4457           <property name="icon_size">4</property>
4458           <property name="xalign">0.5</property>
4459           <property name="yalign">0.5</property>
4460           <property name="xpad">0</property>
4461           <property name="ypad">0</property>
4462         </widget>
4463         <packing>
4464           <property name="padding">0</property>
4465           <property name="expand">False</property>
4466           <property name="fill">False</property>
4467         </packing>
4468       </child>
4469     </widget>
4470   </child>
4471 </widget>
4472
4473 <widget class="GtkDialog" id="DisambiguationErrors">
4474   <property name="width_request">450</property>
4475   <property name="height_request">400</property>
4476   <property name="title" translatable="yes">title</property>
4477   <property name="type">GTK_WINDOW_TOPLEVEL</property>
4478   <property name="window_position">GTK_WIN_POS_NONE</property>
4479   <property name="modal">True</property>
4480   <property name="resizable">True</property>
4481   <property name="destroy_with_parent">False</property>
4482   <property name="decorated">True</property>
4483   <property name="skip_taskbar_hint">False</property>
4484   <property name="skip_pager_hint">False</property>
4485   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
4486   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
4487   <property name="focus_on_map">True</property>
4488   <property name="urgency_hint">False</property>
4489   <property name="has_separator">True</property>
4490
4491   <child internal-child="vbox">
4492     <widget class="GtkVBox" id="vbox14">
4493       <property name="visible">True</property>
4494       <property name="homogeneous">False</property>
4495       <property name="spacing">0</property>
4496
4497       <child internal-child="action_area">
4498         <widget class="GtkHButtonBox" id="hbuttonbox2">
4499           <property name="visible">True</property>
4500           <property name="layout_style">GTK_BUTTONBOX_END</property>
4501
4502           <child>
4503             <widget class="GtkButton" id="button6">
4504               <property name="visible">True</property>
4505               <property name="can_default">True</property>
4506               <property name="can_focus">True</property>
4507               <property name="label">gtk-help</property>
4508               <property name="use_stock">True</property>
4509               <property name="relief">GTK_RELIEF_NORMAL</property>
4510               <property name="focus_on_click">True</property>
4511               <property name="response_id">-11</property>
4512             </widget>
4513           </child>
4514
4515           <child>
4516             <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
4517               <property name="visible">True</property>
4518               <property name="can_default">True</property>
4519               <property name="can_focus">True</property>
4520               <property name="relief">GTK_RELIEF_NORMAL</property>
4521               <property name="focus_on_click">True</property>
4522               <property name="response_id">-6</property>
4523
4524               <child>
4525                 <widget class="GtkAlignment" id="alignment18">
4526                   <property name="visible">True</property>
4527                   <property name="xalign">0.5</property>
4528                   <property name="yalign">0.5</property>
4529                   <property name="xscale">0</property>
4530                   <property name="yscale">0</property>
4531                   <property name="top_padding">0</property>
4532                   <property name="bottom_padding">0</property>
4533                   <property name="left_padding">0</property>
4534                   <property name="right_padding">0</property>
4535
4536                   <child>
4537                     <widget class="GtkHBox" id="hbox29">
4538                       <property name="visible">True</property>
4539                       <property name="homogeneous">False</property>
4540                       <property name="spacing">2</property>
4541
4542                       <child>
4543                         <widget class="GtkImage" id="image926">
4544                           <property name="visible">True</property>
4545                           <property name="stock">gtk-zoom-in</property>
4546                           <property name="icon_size">4</property>
4547                           <property name="xalign">0.5</property>
4548                           <property name="yalign">0.5</property>
4549                           <property name="xpad">0</property>
4550                           <property name="ypad">0</property>
4551                         </widget>
4552                         <packing>
4553                           <property name="padding">0</property>
4554                           <property name="expand">False</property>
4555                           <property name="fill">False</property>
4556                         </packing>
4557                       </child>
4558
4559                       <child>
4560                         <widget class="GtkLabel" id="label28">
4561                           <property name="visible">True</property>
4562                           <property name="label">More</property>
4563                           <property name="use_underline">True</property>
4564                           <property name="use_markup">False</property>
4565                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4566                           <property name="wrap">False</property>
4567                           <property name="selectable">False</property>
4568                           <property name="xalign">0.5</property>
4569                           <property name="yalign">0.5</property>
4570                           <property name="xpad">0</property>
4571                           <property name="ypad">0</property>
4572                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4573                           <property name="width_chars">-1</property>
4574                           <property name="single_line_mode">False</property>
4575                           <property name="angle">0</property>
4576                         </widget>
4577                         <packing>
4578                           <property name="padding">0</property>
4579                           <property name="expand">False</property>
4580                           <property name="fill">False</property>
4581                         </packing>
4582                       </child>
4583                     </widget>
4584                   </child>
4585                 </widget>
4586               </child>
4587             </widget>
4588           </child>
4589
4590           <child>
4591             <widget class="GtkButton" id="disambiguationErrorsCancelButton">
4592               <property name="visible">True</property>
4593               <property name="can_default">True</property>
4594               <property name="has_default">True</property>
4595               <property name="can_focus">True</property>
4596               <property name="label">gtk-cancel</property>
4597               <property name="use_stock">True</property>
4598               <property name="relief">GTK_RELIEF_NORMAL</property>
4599               <property name="focus_on_click">True</property>
4600               <property name="response_id">-6</property>
4601             </widget>
4602           </child>
4603
4604           <child>
4605             <widget class="GtkButton" id="disambiguationErrorsOkButton">
4606               <property name="visible">True</property>
4607               <property name="can_default">True</property>
4608               <property name="can_focus">True</property>
4609               <property name="label">gtk-ok</property>
4610               <property name="use_stock">True</property>
4611               <property name="relief">GTK_RELIEF_NORMAL</property>
4612               <property name="focus_on_click">True</property>
4613               <property name="response_id">-5</property>
4614             </widget>
4615           </child>
4616         </widget>
4617         <packing>
4618           <property name="padding">0</property>
4619           <property name="expand">False</property>
4620           <property name="fill">True</property>
4621           <property name="pack_type">GTK_PACK_END</property>
4622         </packing>
4623       </child>
4624
4625       <child>
4626         <widget class="GtkVBox" id="vbox15">
4627           <property name="visible">True</property>
4628           <property name="homogeneous">False</property>
4629           <property name="spacing">0</property>
4630
4631           <child>
4632             <widget class="GtkLabel" id="disambiguationErrorsLabel">
4633               <property name="visible">True</property>
4634               <property name="label" translatable="yes">some informative message here ...</property>
4635               <property name="use_underline">False</property>
4636               <property name="use_markup">False</property>
4637               <property name="justify">GTK_JUSTIFY_LEFT</property>
4638               <property name="wrap">False</property>
4639               <property name="selectable">False</property>
4640               <property name="xalign">0.5</property>
4641               <property name="yalign">0.5</property>
4642               <property name="xpad">0</property>
4643               <property name="ypad">0</property>
4644               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4645               <property name="width_chars">-1</property>
4646               <property name="single_line_mode">False</property>
4647               <property name="angle">0</property>
4648             </widget>
4649             <packing>
4650               <property name="padding">0</property>
4651               <property name="expand">False</property>
4652               <property name="fill">False</property>
4653             </packing>
4654           </child>
4655
4656           <child>
4657             <widget class="GtkScrolledWindow" id="scrolledwindow12">
4658               <property name="visible">True</property>
4659               <property name="can_focus">True</property>
4660               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4661               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4662               <property name="shadow_type">GTK_SHADOW_IN</property>
4663               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
4664
4665               <child>
4666                 <widget class="GtkTreeView" id="treeview">
4667                   <property name="visible">True</property>
4668                   <property name="can_focus">True</property>
4669                   <property name="headers_visible">False</property>
4670                   <property name="rules_hint">False</property>
4671                   <property name="reorderable">False</property>
4672                   <property name="enable_search">True</property>
4673                   <property name="fixed_height_mode">False</property>
4674                   <property name="hover_selection">False</property>
4675                   <property name="hover_expand">False</property>
4676                 </widget>
4677               </child>
4678             </widget>
4679             <packing>
4680               <property name="padding">0</property>
4681               <property name="expand">True</property>
4682               <property name="fill">True</property>
4683             </packing>
4684           </child>
4685         </widget>
4686         <packing>
4687           <property name="padding">0</property>
4688           <property name="expand">True</property>
4689           <property name="fill">True</property>
4690         </packing>
4691       </child>
4692     </widget>
4693   </child>
4694 </widget>
4695
4696 </glade-interface>