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="GtkToolbar" id="toolbar2">
2348                                   <property name="visible">True</property>
2349                                   <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
2350                                   <property name="toolbar_style">GTK_TOOLBAR_ICONS</property>
2351                                   <property name="tooltips">True</property>
2352                                   <property name="show_arrow">True</property>
2353
2354                                   <child>
2355                                     <widget class="GtkToolItem" id="toolitem46">
2356                                       <property name="visible">True</property>
2357                                       <property name="visible_horizontal">True</property>
2358                                       <property name="visible_vertical">True</property>
2359                                       <property name="is_important">False</property>
2360
2361                                       <child>
2362                                         <widget class="GtkButton" id="scriptAbortButton">
2363                                           <property name="visible">True</property>
2364                                           <property name="can_focus">True</property>
2365                                           <property name="relief">GTK_RELIEF_NONE</property>
2366                                           <property name="focus_on_click">True</property>
2367
2368                                           <child>
2369                                             <widget class="GtkImage" id="image927">
2370                                               <property name="visible">True</property>
2371                                               <property name="stock">gtk-stop</property>
2372                                               <property name="icon_size">4</property>
2373                                               <property name="xalign">0.5</property>
2374                                               <property name="yalign">0.5</property>
2375                                               <property name="xpad">0</property>
2376                                               <property name="ypad">0</property>
2377                                             </widget>
2378                                           </child>
2379                                         </widget>
2380                                       </child>
2381                                     </widget>
2382                                     <packing>
2383                                       <property name="expand">False</property>
2384                                       <property name="homogeneous">False</property>
2385                                     </packing>
2386                                   </child>
2387                                 </widget>
2388                                 <packing>
2389                                   <property name="padding">0</property>
2390                                   <property name="expand">False</property>
2391                                   <property name="fill">True</property>
2392                                 </packing>
2393                               </child>
2394                             </widget>
2395                             <packing>
2396                               <property name="padding">0</property>
2397                               <property name="expand">False</property>
2398                               <property name="fill">False</property>
2399                             </packing>
2400                           </child>
2401
2402                           <child>
2403                             <widget class="GtkNotebook" id="scriptNotebook">
2404                               <property name="visible">True</property>
2405                               <property name="can_focus">True</property>
2406                               <property name="show_tabs">True</property>
2407                               <property name="show_border">True</property>
2408                               <property name="tab_pos">GTK_POS_BOTTOM</property>
2409                               <property name="scrollable">False</property>
2410                               <property name="enable_popup">False</property>
2411
2412                               <child>
2413                                 <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
2414                                   <property name="visible">True</property>
2415                                   <property name="can_focus">True</property>
2416                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2417                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2418                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2419                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2420
2421                                   <child>
2422                                     <placeholder/>
2423                                   </child>
2424                                 </widget>
2425                                 <packing>
2426                                   <property name="tab_expand">False</property>
2427                                   <property name="tab_fill">True</property>
2428                                 </packing>
2429                               </child>
2430
2431                               <child>
2432                                 <widget class="GtkLabel" id="scriptLabel">
2433                                   <property name="visible">True</property>
2434                                   <property name="label" translatable="yes">script</property>
2435                                   <property name="use_underline">False</property>
2436                                   <property name="use_markup">False</property>
2437                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2438                                   <property name="wrap">False</property>
2439                                   <property name="selectable">False</property>
2440                                   <property name="xalign">0.5</property>
2441                                   <property name="yalign">0.5</property>
2442                                   <property name="xpad">0</property>
2443                                   <property name="ypad">0</property>
2444                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2445                                   <property name="width_chars">-1</property>
2446                                   <property name="single_line_mode">False</property>
2447                                   <property name="angle">0</property>
2448                                 </widget>
2449                                 <packing>
2450                                   <property name="type">tab</property>
2451                                 </packing>
2452                               </child>
2453
2454                               <child>
2455                                 <widget class="GtkScrolledWindow" id="scrolledwindow8">
2456                                   <property name="visible">True</property>
2457                                   <property name="can_focus">True</property>
2458                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2459                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2460                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2461                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2462
2463                                   <child>
2464                                     <widget class="GtkViewport" id="viewport1">
2465                                       <property name="visible">True</property>
2466                                       <property name="shadow_type">GTK_SHADOW_IN</property>
2467
2468                                       <child>
2469                                         <widget class="GtkLabel" id="label25">
2470                                           <property name="visible">True</property>
2471                                           <property name="label" translatable="yes">Not implemented.</property>
2472                                           <property name="use_underline">False</property>
2473                                           <property name="use_markup">False</property>
2474                                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2475                                           <property name="wrap">False</property>
2476                                           <property name="selectable">False</property>
2477                                           <property name="xalign">0.5</property>
2478                                           <property name="yalign">0.5</property>
2479                                           <property name="xpad">0</property>
2480                                           <property name="ypad">0</property>
2481                                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2482                                           <property name="width_chars">-1</property>
2483                                           <property name="single_line_mode">False</property>
2484                                           <property name="angle">0</property>
2485                                         </widget>
2486                                       </child>
2487                                     </widget>
2488                                   </child>
2489                                 </widget>
2490                                 <packing>
2491                                   <property name="tab_expand">False</property>
2492                                   <property name="tab_fill">True</property>
2493                                 </packing>
2494                               </child>
2495
2496                               <child>
2497                                 <widget class="GtkLabel" id="label13">
2498                                   <property name="visible">True</property>
2499                                   <property name="label" translatable="yes">outline</property>
2500                                   <property name="use_underline">False</property>
2501                                   <property name="use_markup">False</property>
2502                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2503                                   <property name="wrap">False</property>
2504                                   <property name="selectable">False</property>
2505                                   <property name="xalign">0.5</property>
2506                                   <property name="yalign">0.5</property>
2507                                   <property name="xpad">0</property>
2508                                   <property name="ypad">0</property>
2509                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2510                                   <property name="width_chars">-1</property>
2511                                   <property name="single_line_mode">False</property>
2512                                   <property name="angle">0</property>
2513                                 </widget>
2514                                 <packing>
2515                                   <property name="type">tab</property>
2516                                 </packing>
2517                               </child>
2518                             </widget>
2519                             <packing>
2520                               <property name="padding">0</property>
2521                               <property name="expand">True</property>
2522                               <property name="fill">True</property>
2523                             </packing>
2524                           </child>
2525                         </widget>
2526                         <packing>
2527                           <property name="padding">0</property>
2528                           <property name="expand">True</property>
2529                           <property name="fill">True</property>
2530                         </packing>
2531                       </child>
2532                     </widget>
2533                     <packing>
2534                       <property name="shrink">True</property>
2535                       <property name="resize">False</property>
2536                     </packing>
2537                   </child>
2538
2539                   <child>
2540                     <widget class="GtkVPaned" id="vpaned1">
2541                       <property name="width_request">250</property>
2542                       <property name="height_request">500</property>
2543                       <property name="visible">True</property>
2544                       <property name="can_focus">True</property>
2545                       <property name="position">380</property>
2546
2547                       <child>
2548                         <widget class="GtkNotebook" id="sequentsNotebook">
2549                           <property name="visible">True</property>
2550                           <property name="can_focus">True</property>
2551                           <property name="show_tabs">True</property>
2552                           <property name="show_border">True</property>
2553                           <property name="tab_pos">GTK_POS_TOP</property>
2554                           <property name="scrollable">False</property>
2555                           <property name="enable_popup">False</property>
2556                         </widget>
2557                         <packing>
2558                           <property name="shrink">True</property>
2559                           <property name="resize">False</property>
2560                         </packing>
2561                       </child>
2562
2563                       <child>
2564                         <widget class="GtkHBox" id="hbox9">
2565                           <property name="visible">True</property>
2566                           <property name="homogeneous">False</property>
2567                           <property name="spacing">0</property>
2568
2569                           <child>
2570                             <widget class="GtkScrolledWindow" id="logScrolledWin">
2571                               <property name="visible">True</property>
2572                               <property name="can_focus">True</property>
2573                               <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
2574                               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2575                               <property name="shadow_type">GTK_SHADOW_IN</property>
2576                               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2577
2578                               <child>
2579                                 <widget class="GtkTextView" id="logTextView">
2580                                   <property name="visible">True</property>
2581                                   <property name="can_focus">True</property>
2582                                   <property name="editable">False</property>
2583                                   <property name="overwrite">False</property>
2584                                   <property name="accepts_tab">True</property>
2585                                   <property name="justification">GTK_JUSTIFY_LEFT</property>
2586                                   <property name="wrap_mode">GTK_WRAP_CHAR</property>
2587                                   <property name="cursor_visible">False</property>
2588                                   <property name="pixels_above_lines">0</property>
2589                                   <property name="pixels_below_lines">0</property>
2590                                   <property name="pixels_inside_wrap">0</property>
2591                                   <property name="left_margin">0</property>
2592                                   <property name="right_margin">0</property>
2593                                   <property name="indent">0</property>
2594                                   <property name="text" translatable="yes"></property>
2595                                 </widget>
2596                               </child>
2597                             </widget>
2598                             <packing>
2599                               <property name="padding">0</property>
2600                               <property name="expand">True</property>
2601                               <property name="fill">True</property>
2602                             </packing>
2603                           </child>
2604                         </widget>
2605                         <packing>
2606                           <property name="shrink">True</property>
2607                           <property name="resize">True</property>
2608                         </packing>
2609                       </child>
2610                     </widget>
2611                     <packing>
2612                       <property name="shrink">True</property>
2613                       <property name="resize">True</property>
2614                     </packing>
2615                   </child>
2616                 </widget>
2617                 <packing>
2618                   <property name="padding">0</property>
2619                   <property name="expand">True</property>
2620                   <property name="fill">True</property>
2621                 </packing>
2622               </child>
2623             </widget>
2624             <packing>
2625               <property name="padding">0</property>
2626               <property name="expand">True</property>
2627               <property name="fill">True</property>
2628             </packing>
2629           </child>
2630
2631           <child>
2632             <widget class="GtkHBox" id="hbox10">
2633               <property name="visible">True</property>
2634               <property name="homogeneous">False</property>
2635               <property name="spacing">0</property>
2636
2637               <child>
2638                 <widget class="GtkStatusbar" id="StatusBar">
2639                   <property name="visible">True</property>
2640                   <property name="has_resize_grip">False</property>
2641                 </widget>
2642                 <packing>
2643                   <property name="padding">0</property>
2644                   <property name="expand">True</property>
2645                   <property name="fill">True</property>
2646                 </packing>
2647               </child>
2648
2649               <child>
2650                 <widget class="GtkNotebook" id="HintNotebook">
2651                   <property name="visible">True</property>
2652                   <property name="show_tabs">False</property>
2653                   <property name="show_border">True</property>
2654                   <property name="tab_pos">GTK_POS_TOP</property>
2655                   <property name="scrollable">False</property>
2656                   <property name="enable_popup">False</property>
2657
2658                   <child>
2659                     <widget class="GtkImage" id="HintLowImage">
2660                       <property name="visible">True</property>
2661                       <property name="xalign">0.5</property>
2662                       <property name="yalign">0.5</property>
2663                       <property name="xpad">0</property>
2664                       <property name="ypad">0</property>
2665                     </widget>
2666                     <packing>
2667                       <property name="tab_expand">False</property>
2668                       <property name="tab_fill">True</property>
2669                     </packing>
2670                   </child>
2671
2672                   <child>
2673                     <widget class="GtkLabel" id="label14">
2674                       <property name="visible">True</property>
2675                       <property name="label" translatable="yes">label14</property>
2676                       <property name="use_underline">False</property>
2677                       <property name="use_markup">False</property>
2678                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2679                       <property name="wrap">False</property>
2680                       <property name="selectable">False</property>
2681                       <property name="xalign">0.5</property>
2682                       <property name="yalign">0.5</property>
2683                       <property name="xpad">0</property>
2684                       <property name="ypad">0</property>
2685                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2686                       <property name="width_chars">-1</property>
2687                       <property name="single_line_mode">False</property>
2688                       <property name="angle">0</property>
2689                     </widget>
2690                     <packing>
2691                       <property name="type">tab</property>
2692                     </packing>
2693                   </child>
2694
2695                   <child>
2696                     <widget class="GtkImage" id="HintMediumImage">
2697                       <property name="visible">True</property>
2698                       <property name="xalign">0.5</property>
2699                       <property name="yalign">0.5</property>
2700                       <property name="xpad">0</property>
2701                       <property name="ypad">0</property>
2702                     </widget>
2703                     <packing>
2704                       <property name="tab_expand">False</property>
2705                       <property name="tab_fill">True</property>
2706                     </packing>
2707                   </child>
2708
2709                   <child>
2710                     <widget class="GtkLabel" id="label15">
2711                       <property name="visible">True</property>
2712                       <property name="label" translatable="yes">label15</property>
2713                       <property name="use_underline">False</property>
2714                       <property name="use_markup">False</property>
2715                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2716                       <property name="wrap">False</property>
2717                       <property name="selectable">False</property>
2718                       <property name="xalign">0.5</property>
2719                       <property name="yalign">0.5</property>
2720                       <property name="xpad">0</property>
2721                       <property name="ypad">0</property>
2722                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2723                       <property name="width_chars">-1</property>
2724                       <property name="single_line_mode">False</property>
2725                       <property name="angle">0</property>
2726                     </widget>
2727                     <packing>
2728                       <property name="type">tab</property>
2729                     </packing>
2730                   </child>
2731
2732                   <child>
2733                     <widget class="GtkImage" id="HintHighImage">
2734                       <property name="visible">True</property>
2735                       <property name="xalign">0.5</property>
2736                       <property name="yalign">0.5</property>
2737                       <property name="xpad">0</property>
2738                       <property name="ypad">0</property>
2739                     </widget>
2740                     <packing>
2741                       <property name="tab_expand">False</property>
2742                       <property name="tab_fill">True</property>
2743                     </packing>
2744                   </child>
2745
2746                   <child>
2747                     <widget class="GtkLabel" id="label16">
2748                       <property name="visible">True</property>
2749                       <property name="label" translatable="yes">label16</property>
2750                       <property name="use_underline">False</property>
2751                       <property name="use_markup">False</property>
2752                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2753                       <property name="wrap">False</property>
2754                       <property name="selectable">False</property>
2755                       <property name="xalign">0.5</property>
2756                       <property name="yalign">0.5</property>
2757                       <property name="xpad">0</property>
2758                       <property name="ypad">0</property>
2759                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2760                       <property name="width_chars">-1</property>
2761                       <property name="single_line_mode">False</property>
2762                       <property name="angle">0</property>
2763                     </widget>
2764                     <packing>
2765                       <property name="type">tab</property>
2766                     </packing>
2767                   </child>
2768                 </widget>
2769                 <packing>
2770                   <property name="padding">0</property>
2771                   <property name="expand">False</property>
2772                   <property name="fill">True</property>
2773                 </packing>
2774               </child>
2775             </widget>
2776             <packing>
2777               <property name="padding">0</property>
2778               <property name="expand">False</property>
2779               <property name="fill">False</property>
2780             </packing>
2781           </child>
2782         </widget>
2783       </child>
2784     </widget>
2785   </child>
2786 </widget>
2787
2788 <widget class="GtkDialog" id="TextDialog">
2789   <property name="title" translatable="yes">DUMMY</property>
2790   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2791   <property name="window_position">GTK_WIN_POS_NONE</property>
2792   <property name="modal">False</property>
2793   <property name="resizable">True</property>
2794   <property name="destroy_with_parent">False</property>
2795   <property name="decorated">True</property>
2796   <property name="skip_taskbar_hint">False</property>
2797   <property name="skip_pager_hint">False</property>
2798   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2799   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2800   <property name="focus_on_map">True</property>
2801   <property name="urgency_hint">False</property>
2802   <property name="has_separator">True</property>
2803
2804   <child internal-child="vbox">
2805     <widget class="GtkVBox" id="vbox5">
2806       <property name="visible">True</property>
2807       <property name="homogeneous">False</property>
2808       <property name="spacing">0</property>
2809
2810       <child internal-child="action_area">
2811         <widget class="GtkHButtonBox" id="hbuttonbox1">
2812           <property name="visible">True</property>
2813           <property name="layout_style">GTK_BUTTONBOX_END</property>
2814
2815           <child>
2816             <widget class="GtkButton" id="TextDialogCancelButton">
2817               <property name="visible">True</property>
2818               <property name="can_default">True</property>
2819               <property name="can_focus">True</property>
2820               <property name="label">gtk-cancel</property>
2821               <property name="use_stock">True</property>
2822               <property name="relief">GTK_RELIEF_NORMAL</property>
2823               <property name="focus_on_click">True</property>
2824               <property name="response_id">-6</property>
2825             </widget>
2826           </child>
2827
2828           <child>
2829             <widget class="GtkButton" id="TextDialogOkButton">
2830               <property name="visible">True</property>
2831               <property name="can_default">True</property>
2832               <property name="can_focus">True</property>
2833               <property name="label">gtk-ok</property>
2834               <property name="use_stock">True</property>
2835               <property name="relief">GTK_RELIEF_NORMAL</property>
2836               <property name="focus_on_click">True</property>
2837               <property name="response_id">-5</property>
2838             </widget>
2839           </child>
2840         </widget>
2841         <packing>
2842           <property name="padding">0</property>
2843           <property name="expand">False</property>
2844           <property name="fill">True</property>
2845           <property name="pack_type">GTK_PACK_END</property>
2846         </packing>
2847       </child>
2848
2849       <child>
2850         <widget class="GtkLabel" id="TextDialogLabel">
2851           <property name="visible">True</property>
2852           <property name="label" translatable="yes">DUMMY</property>
2853           <property name="use_underline">False</property>
2854           <property name="use_markup">False</property>
2855           <property name="justify">GTK_JUSTIFY_LEFT</property>
2856           <property name="wrap">False</property>
2857           <property name="selectable">False</property>
2858           <property name="xalign">0.5</property>
2859           <property name="yalign">0.5</property>
2860           <property name="xpad">0</property>
2861           <property name="ypad">0</property>
2862           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2863           <property name="width_chars">-1</property>
2864           <property name="single_line_mode">False</property>
2865           <property name="angle">0</property>
2866         </widget>
2867         <packing>
2868           <property name="padding">0</property>
2869           <property name="expand">False</property>
2870           <property name="fill">False</property>
2871         </packing>
2872       </child>
2873
2874       <child>
2875         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2876           <property name="visible">True</property>
2877           <property name="can_focus">True</property>
2878           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2879           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2880           <property name="shadow_type">GTK_SHADOW_IN</property>
2881           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2882
2883           <child>
2884             <widget class="GtkTextView" id="TextDialogTextView">
2885               <property name="visible">True</property>
2886               <property name="can_focus">True</property>
2887               <property name="editable">True</property>
2888               <property name="overwrite">False</property>
2889               <property name="accepts_tab">True</property>
2890               <property name="justification">GTK_JUSTIFY_LEFT</property>
2891               <property name="wrap_mode">GTK_WRAP_NONE</property>
2892               <property name="cursor_visible">True</property>
2893               <property name="pixels_above_lines">0</property>
2894               <property name="pixels_below_lines">0</property>
2895               <property name="pixels_inside_wrap">0</property>
2896               <property name="left_margin">0</property>
2897               <property name="right_margin">0</property>
2898               <property name="indent">0</property>
2899               <property name="text" translatable="yes"></property>
2900             </widget>
2901           </child>
2902         </widget>
2903         <packing>
2904           <property name="padding">0</property>
2905           <property name="expand">True</property>
2906           <property name="fill">True</property>
2907         </packing>
2908       </child>
2909     </widget>
2910   </child>
2911 </widget>
2912
2913 <widget class="GtkDialog" id="UriChoiceDialog">
2914   <property name="height_request">280</property>
2915   <property name="title" translatable="yes">Uri choice</property>
2916   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2917   <property name="window_position">GTK_WIN_POS_CENTER</property>
2918   <property name="modal">True</property>
2919   <property name="resizable">True</property>
2920   <property name="destroy_with_parent">False</property>
2921   <property name="decorated">True</property>
2922   <property name="skip_taskbar_hint">False</property>
2923   <property name="skip_pager_hint">False</property>
2924   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2925   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2926   <property name="focus_on_map">True</property>
2927   <property name="urgency_hint">False</property>
2928   <property name="has_separator">True</property>
2929
2930   <child internal-child="vbox">
2931     <widget class="GtkVBox" id="dialog-vbox3">
2932       <property name="visible">True</property>
2933       <property name="homogeneous">False</property>
2934       <property name="spacing">4</property>
2935
2936       <child internal-child="action_area">
2937         <widget class="GtkHButtonBox" id="dialog-action_area3">
2938           <property name="visible">True</property>
2939           <property name="layout_style">GTK_BUTTONBOX_END</property>
2940
2941           <child>
2942             <widget class="GtkButton" id="UriChoiceAbortButton">
2943               <property name="visible">True</property>
2944               <property name="can_default">True</property>
2945               <property name="can_focus">True</property>
2946               <property name="label">gtk-cancel</property>
2947               <property name="use_stock">True</property>
2948               <property name="relief">GTK_RELIEF_NORMAL</property>
2949               <property name="focus_on_click">True</property>
2950               <property name="response_id">-6</property>
2951             </widget>
2952           </child>
2953
2954           <child>
2955             <widget class="GtkButton" id="UriChoiceSelectedButton">
2956               <property name="visible">True</property>
2957               <property name="can_default">True</property>
2958               <property name="can_focus">True</property>
2959               <property name="relief">GTK_RELIEF_NORMAL</property>
2960               <property name="focus_on_click">True</property>
2961               <property name="response_id">0</property>
2962
2963               <child>
2964                 <widget class="GtkAlignment" id="alignment2">
2965                   <property name="visible">True</property>
2966                   <property name="xalign">0.5</property>
2967                   <property name="yalign">0.5</property>
2968                   <property name="xscale">0</property>
2969                   <property name="yscale">0</property>
2970                   <property name="top_padding">0</property>
2971                   <property name="bottom_padding">0</property>
2972                   <property name="left_padding">0</property>
2973                   <property name="right_padding">0</property>
2974
2975                   <child>
2976                     <widget class="GtkHBox" id="hbox3">
2977                       <property name="visible">True</property>
2978                       <property name="homogeneous">False</property>
2979                       <property name="spacing">2</property>
2980
2981                       <child>
2982                         <widget class="GtkImage" id="image19">
2983                           <property name="visible">True</property>
2984                           <property name="stock">gtk-index</property>
2985                           <property name="icon_size">4</property>
2986                           <property name="xalign">0.5</property>
2987                           <property name="yalign">0.5</property>
2988                           <property name="xpad">0</property>
2989                           <property name="ypad">0</property>
2990                         </widget>
2991                         <packing>
2992                           <property name="padding">0</property>
2993                           <property name="expand">False</property>
2994                           <property name="fill">False</property>
2995                         </packing>
2996                       </child>
2997
2998                       <child>
2999                         <widget class="GtkLabel" id="label3">
3000                           <property name="visible">True</property>
3001                           <property name="label" translatable="yes">Try _Selected</property>
3002                           <property name="use_underline">True</property>
3003                           <property name="use_markup">False</property>
3004                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3005                           <property name="wrap">False</property>
3006                           <property name="selectable">False</property>
3007                           <property name="xalign">0.5</property>
3008                           <property name="yalign">0.5</property>
3009                           <property name="xpad">0</property>
3010                           <property name="ypad">0</property>
3011                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3012                           <property name="width_chars">-1</property>
3013                           <property name="single_line_mode">False</property>
3014                           <property name="angle">0</property>
3015                         </widget>
3016                         <packing>
3017                           <property name="padding">0</property>
3018                           <property name="expand">False</property>
3019                           <property name="fill">False</property>
3020                         </packing>
3021                       </child>
3022                     </widget>
3023                   </child>
3024                 </widget>
3025               </child>
3026             </widget>
3027           </child>
3028
3029           <child>
3030             <widget class="GtkButton" id="UriChoiceConstantsButton">
3031               <property name="visible">True</property>
3032               <property name="sensitive">False</property>
3033               <property name="can_default">True</property>
3034               <property name="can_focus">True</property>
3035               <property name="label" translatable="yes">Try Constants</property>
3036               <property name="use_underline">True</property>
3037               <property name="relief">GTK_RELIEF_NORMAL</property>
3038               <property name="focus_on_click">True</property>
3039               <property name="response_id">0</property>
3040             </widget>
3041           </child>
3042
3043           <child>
3044             <widget class="GtkButton" id="copyButton">
3045               <property name="can_default">True</property>
3046               <property name="can_focus">True</property>
3047               <property name="label">gtk-copy</property>
3048               <property name="use_stock">True</property>
3049               <property name="relief">GTK_RELIEF_NORMAL</property>
3050               <property name="focus_on_click">True</property>
3051               <property name="response_id">0</property>
3052             </widget>
3053           </child>
3054
3055           <child>
3056             <widget class="GtkButton" id="uriChoiceAutoButton">
3057               <property name="visible">True</property>
3058               <property name="can_default">True</property>
3059               <property name="can_focus">True</property>
3060               <property name="relief">GTK_RELIEF_NORMAL</property>
3061               <property name="focus_on_click">True</property>
3062               <property name="response_id">0</property>
3063
3064               <child>
3065                 <widget class="GtkAlignment" id="alignment5">
3066                   <property name="visible">True</property>
3067                   <property name="xalign">0.5</property>
3068                   <property name="yalign">0.5</property>
3069                   <property name="xscale">0</property>
3070                   <property name="yscale">0</property>
3071                   <property name="top_padding">0</property>
3072                   <property name="bottom_padding">0</property>
3073                   <property name="left_padding">0</property>
3074                   <property name="right_padding">0</property>
3075
3076                   <child>
3077                     <widget class="GtkHBox" id="hbox16">
3078                       <property name="visible">True</property>
3079                       <property name="homogeneous">False</property>
3080                       <property name="spacing">2</property>
3081
3082                       <child>
3083                         <widget class="GtkImage" id="image302">
3084                           <property name="visible">True</property>
3085                           <property name="stock">gtk-ok</property>
3086                           <property name="icon_size">4</property>
3087                           <property name="xalign">0.5</property>
3088                           <property name="yalign">0.5</property>
3089                           <property name="xpad">0</property>
3090                           <property name="ypad">0</property>
3091                         </widget>
3092                         <packing>
3093                           <property name="padding">0</property>
3094                           <property name="expand">False</property>
3095                           <property name="fill">False</property>
3096                         </packing>
3097                       </child>
3098
3099                       <child>
3100                         <widget class="GtkLabel" id="okLabel">
3101                           <property name="visible">True</property>
3102                           <property name="label" translatable="yes">bla bla bla</property>
3103                           <property name="use_underline">True</property>
3104                           <property name="use_markup">False</property>
3105                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3106                           <property name="wrap">False</property>
3107                           <property name="selectable">False</property>
3108                           <property name="xalign">0.5</property>
3109                           <property name="yalign">0.5</property>
3110                           <property name="xpad">0</property>
3111                           <property name="ypad">0</property>
3112                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3113                           <property name="width_chars">-1</property>
3114                           <property name="single_line_mode">False</property>
3115                           <property name="angle">0</property>
3116                         </widget>
3117                         <packing>
3118                           <property name="padding">0</property>
3119                           <property name="expand">False</property>
3120                           <property name="fill">False</property>
3121                         </packing>
3122                       </child>
3123                     </widget>
3124                   </child>
3125                 </widget>
3126               </child>
3127             </widget>
3128           </child>
3129
3130           <child>
3131             <widget class="GtkButton" id="uriChoiceForwardButton">
3132               <property name="visible">True</property>
3133               <property name="can_default">True</property>
3134               <property name="can_focus">True</property>
3135               <property name="label">gtk-go-forward</property>
3136               <property name="use_stock">True</property>
3137               <property name="relief">GTK_RELIEF_NORMAL</property>
3138               <property name="focus_on_click">True</property>
3139               <property name="response_id">0</property>
3140             </widget>
3141           </child>
3142         </widget>
3143         <packing>
3144           <property name="padding">0</property>
3145           <property name="expand">False</property>
3146           <property name="fill">True</property>
3147           <property name="pack_type">GTK_PACK_END</property>
3148         </packing>
3149       </child>
3150
3151       <child>
3152         <widget class="GtkVBox" id="vbox2">
3153           <property name="visible">True</property>
3154           <property name="homogeneous">False</property>
3155           <property name="spacing">3</property>
3156
3157           <child>
3158             <widget class="GtkLabel" id="UriChoiceLabel">
3159               <property name="visible">True</property>
3160               <property name="label" translatable="yes">some informative message here ...</property>
3161               <property name="use_underline">False</property>
3162               <property name="use_markup">False</property>
3163               <property name="justify">GTK_JUSTIFY_LEFT</property>
3164               <property name="wrap">False</property>
3165               <property name="selectable">False</property>
3166               <property name="xalign">0.5</property>
3167               <property name="yalign">0.5</property>
3168               <property name="xpad">0</property>
3169               <property name="ypad">0</property>
3170               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3171               <property name="width_chars">-1</property>
3172               <property name="single_line_mode">False</property>
3173               <property name="angle">0</property>
3174             </widget>
3175             <packing>
3176               <property name="padding">0</property>
3177               <property name="expand">False</property>
3178               <property name="fill">False</property>
3179             </packing>
3180           </child>
3181
3182           <child>
3183             <widget class="GtkScrolledWindow" id="scrolledwindow1">
3184               <property name="width_request">400</property>
3185               <property name="visible">True</property>
3186               <property name="can_focus">True</property>
3187               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3188               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3189               <property name="shadow_type">GTK_SHADOW_NONE</property>
3190               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3191
3192               <child>
3193                 <widget class="GtkTreeView" id="UriChoiceTreeView">
3194                   <property name="visible">True</property>
3195                   <property name="can_focus">True</property>
3196                   <property name="headers_visible">False</property>
3197                   <property name="rules_hint">False</property>
3198                   <property name="reorderable">False</property>
3199                   <property name="enable_search">True</property>
3200                   <property name="fixed_height_mode">False</property>
3201                   <property name="hover_selection">False</property>
3202                   <property name="hover_expand">False</property>
3203                 </widget>
3204               </child>
3205             </widget>
3206             <packing>
3207               <property name="padding">0</property>
3208               <property name="expand">True</property>
3209               <property name="fill">True</property>
3210             </packing>
3211           </child>
3212
3213           <child>
3214             <widget class="GtkHBox" id="uriEntryHBox">
3215               <property name="visible">True</property>
3216               <property name="homogeneous">False</property>
3217               <property name="spacing">0</property>
3218
3219               <child>
3220                 <widget class="GtkLabel" id="label2">
3221                   <property name="visible">True</property>
3222                   <property name="label" translatable="yes">URI: </property>
3223                   <property name="use_underline">False</property>
3224                   <property name="use_markup">False</property>
3225                   <property name="justify">GTK_JUSTIFY_LEFT</property>
3226                   <property name="wrap">False</property>
3227                   <property name="selectable">False</property>
3228                   <property name="xalign">0.5</property>
3229                   <property name="yalign">0.5</property>
3230                   <property name="xpad">0</property>
3231                   <property name="ypad">0</property>
3232                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3233                   <property name="width_chars">-1</property>
3234                   <property name="single_line_mode">False</property>
3235                   <property name="angle">0</property>
3236                 </widget>
3237                 <packing>
3238                   <property name="padding">0</property>
3239                   <property name="expand">False</property>
3240                   <property name="fill">False</property>
3241                 </packing>
3242               </child>
3243
3244               <child>
3245                 <widget class="GtkEntry" id="entry1">
3246                   <property name="visible">True</property>
3247                   <property name="can_focus">True</property>
3248                   <property name="editable">True</property>
3249                   <property name="visibility">True</property>
3250                   <property name="max_length">0</property>
3251                   <property name="text" translatable="yes"></property>
3252                   <property name="has_frame">True</property>
3253                   <property name="invisible_char">*</property>
3254                   <property name="activates_default">False</property>
3255                 </widget>
3256                 <packing>
3257                   <property name="padding">0</property>
3258                   <property name="expand">True</property>
3259                   <property name="fill">True</property>
3260                 </packing>
3261               </child>
3262             </widget>
3263             <packing>
3264               <property name="padding">0</property>
3265               <property name="expand">False</property>
3266               <property name="fill">True</property>
3267             </packing>
3268           </child>
3269         </widget>
3270         <packing>
3271           <property name="padding">0</property>
3272           <property name="expand">True</property>
3273           <property name="fill">True</property>
3274         </packing>
3275       </child>
3276     </widget>
3277   </child>
3278 </widget>
3279
3280 <widget class="GtkWindow" id="FindReplWin">
3281   <property name="border_width">5</property>
3282   <property name="title" translatable="yes">Find &amp; Replace</property>
3283   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3284   <property name="window_position">GTK_WIN_POS_MOUSE</property>
3285   <property name="modal">False</property>
3286   <property name="resizable">False</property>
3287   <property name="destroy_with_parent">False</property>
3288   <property name="decorated">True</property>
3289   <property name="skip_taskbar_hint">False</property>
3290   <property name="skip_pager_hint">False</property>
3291   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3292   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3293   <property name="focus_on_map">True</property>
3294   <property name="urgency_hint">False</property>
3295
3296   <child>
3297     <widget class="GtkTable" id="table1">
3298       <property name="visible">True</property>
3299       <property name="n_rows">3</property>
3300       <property name="n_columns">2</property>
3301       <property name="homogeneous">False</property>
3302       <property name="row_spacing">5</property>
3303       <property name="column_spacing">0</property>
3304
3305       <child>
3306         <widget class="GtkLabel" id="label17">
3307           <property name="visible">True</property>
3308           <property name="label" translatable="yes">Find:</property>
3309           <property name="use_underline">False</property>
3310           <property name="use_markup">False</property>
3311           <property name="justify">GTK_JUSTIFY_LEFT</property>
3312           <property name="wrap">False</property>
3313           <property name="selectable">False</property>
3314           <property name="xalign">0</property>
3315           <property name="yalign">0.5</property>
3316           <property name="xpad">0</property>
3317           <property name="ypad">0</property>
3318           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3319           <property name="width_chars">-1</property>
3320           <property name="single_line_mode">False</property>
3321           <property name="angle">0</property>
3322         </widget>
3323         <packing>
3324           <property name="left_attach">0</property>
3325           <property name="right_attach">1</property>
3326           <property name="top_attach">0</property>
3327           <property name="bottom_attach">1</property>
3328           <property name="x_options">fill</property>
3329           <property name="y_options"></property>
3330         </packing>
3331       </child>
3332
3333       <child>
3334         <widget class="GtkLabel" id="label18">
3335           <property name="visible">True</property>
3336           <property name="label" translatable="yes">Replace with: </property>
3337           <property name="use_underline">False</property>
3338           <property name="use_markup">False</property>
3339           <property name="justify">GTK_JUSTIFY_LEFT</property>
3340           <property name="wrap">False</property>
3341           <property name="selectable">False</property>
3342           <property name="xalign">0</property>
3343           <property name="yalign">0.5</property>
3344           <property name="xpad">0</property>
3345           <property name="ypad">0</property>
3346           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3347           <property name="width_chars">-1</property>
3348           <property name="single_line_mode">False</property>
3349           <property name="angle">0</property>
3350         </widget>
3351         <packing>
3352           <property name="left_attach">0</property>
3353           <property name="right_attach">1</property>
3354           <property name="top_attach">1</property>
3355           <property name="bottom_attach">2</property>
3356           <property name="x_options">fill</property>
3357           <property name="y_options"></property>
3358         </packing>
3359       </child>
3360
3361       <child>
3362         <widget class="GtkEntry" id="findEntry">
3363           <property name="visible">True</property>
3364           <property name="can_default">True</property>
3365           <property name="has_default">True</property>
3366           <property name="can_focus">True</property>
3367           <property name="has_focus">True</property>
3368           <property name="editable">True</property>
3369           <property name="visibility">True</property>
3370           <property name="max_length">0</property>
3371           <property name="text" translatable="yes"></property>
3372           <property name="has_frame">True</property>
3373           <property name="invisible_char">*</property>
3374           <property name="activates_default">False</property>
3375         </widget>
3376         <packing>
3377           <property name="left_attach">1</property>
3378           <property name="right_attach">2</property>
3379           <property name="top_attach">0</property>
3380           <property name="bottom_attach">1</property>
3381           <property name="y_options"></property>
3382         </packing>
3383       </child>
3384
3385       <child>
3386         <widget class="GtkEntry" id="replaceEntry">
3387           <property name="visible">True</property>
3388           <property name="can_focus">True</property>
3389           <property name="editable">True</property>
3390           <property name="visibility">True</property>
3391           <property name="max_length">0</property>
3392           <property name="text" translatable="yes"></property>
3393           <property name="has_frame">True</property>
3394           <property name="invisible_char">*</property>
3395           <property name="activates_default">False</property>
3396         </widget>
3397         <packing>
3398           <property name="left_attach">1</property>
3399           <property name="right_attach">2</property>
3400           <property name="top_attach">1</property>
3401           <property name="bottom_attach">2</property>
3402           <property name="y_options"></property>
3403         </packing>
3404       </child>
3405
3406       <child>
3407         <widget class="GtkHBox" id="hbox19">
3408           <property name="visible">True</property>
3409           <property name="homogeneous">False</property>
3410           <property name="spacing">5</property>
3411
3412           <child>
3413             <widget class="GtkVBox" id="vbox9">
3414               <property name="visible">True</property>
3415               <property name="homogeneous">False</property>
3416               <property name="spacing">0</property>
3417
3418               <child>
3419                 <placeholder/>
3420               </child>
3421
3422               <child>
3423                 <placeholder/>
3424               </child>
3425             </widget>
3426             <packing>
3427               <property name="padding">0</property>
3428               <property name="expand">True</property>
3429               <property name="fill">True</property>
3430             </packing>
3431           </child>
3432
3433           <child>
3434             <widget class="GtkButton" id="findButton">
3435               <property name="visible">True</property>
3436               <property name="can_focus">True</property>
3437               <property name="label">gtk-find</property>
3438               <property name="use_stock">True</property>
3439               <property name="relief">GTK_RELIEF_NORMAL</property>
3440               <property name="focus_on_click">True</property>
3441             </widget>
3442             <packing>
3443               <property name="padding">0</property>
3444               <property name="expand">False</property>
3445               <property name="fill">False</property>
3446             </packing>
3447           </child>
3448
3449           <child>
3450             <widget class="GtkButton" id="findReplButton">
3451               <property name="visible">True</property>
3452               <property name="can_focus">True</property>
3453               <property name="relief">GTK_RELIEF_NORMAL</property>
3454               <property name="focus_on_click">True</property>
3455
3456               <child>
3457                 <widget class="GtkAlignment" id="alignment13">
3458                   <property name="visible">True</property>
3459                   <property name="xalign">0.5</property>
3460                   <property name="yalign">0.5</property>
3461                   <property name="xscale">0</property>
3462                   <property name="yscale">0</property>
3463                   <property name="top_padding">0</property>
3464                   <property name="bottom_padding">0</property>
3465                   <property name="left_padding">0</property>
3466                   <property name="right_padding">0</property>
3467
3468                   <child>
3469                     <widget class="GtkHBox" id="hbox20">
3470                       <property name="visible">True</property>
3471                       <property name="homogeneous">False</property>
3472                       <property name="spacing">2</property>
3473
3474                       <child>
3475                         <widget class="GtkImage" id="image357">
3476                           <property name="visible">True</property>
3477                           <property name="stock">gtk-find-and-replace</property>
3478                           <property name="icon_size">4</property>
3479                           <property name="xalign">0.5</property>
3480                           <property name="yalign">0.5</property>
3481                           <property name="xpad">0</property>
3482                           <property name="ypad">0</property>
3483                         </widget>
3484                         <packing>
3485                           <property name="padding">0</property>
3486                           <property name="expand">False</property>
3487                           <property name="fill">False</property>
3488                         </packing>
3489                       </child>
3490
3491                       <child>
3492                         <widget class="GtkLabel" id="label19">
3493                           <property name="visible">True</property>
3494                           <property name="label">_Replace</property>
3495                           <property name="use_underline">True</property>
3496                           <property name="use_markup">False</property>
3497                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3498                           <property name="wrap">False</property>
3499                           <property name="selectable">False</property>
3500                           <property name="xalign">0.5</property>
3501                           <property name="yalign">0.5</property>
3502                           <property name="xpad">0</property>
3503                           <property name="ypad">0</property>
3504                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3505                           <property name="width_chars">-1</property>
3506                           <property name="single_line_mode">False</property>
3507                           <property name="angle">0</property>
3508                         </widget>
3509                         <packing>
3510                           <property name="padding">0</property>
3511                           <property name="expand">False</property>
3512                           <property name="fill">False</property>
3513                         </packing>
3514                       </child>
3515                     </widget>
3516                   </child>
3517                 </widget>
3518               </child>
3519             </widget>
3520             <packing>
3521               <property name="padding">0</property>
3522               <property name="expand">False</property>
3523               <property name="fill">False</property>
3524             </packing>
3525           </child>
3526
3527           <child>
3528             <widget class="GtkButton" id="cancelButton">
3529               <property name="visible">True</property>
3530               <property name="can_focus">True</property>
3531               <property name="label">gtk-cancel</property>
3532               <property name="use_stock">True</property>
3533               <property name="relief">GTK_RELIEF_NORMAL</property>
3534               <property name="focus_on_click">True</property>
3535             </widget>
3536             <packing>
3537               <property name="padding">0</property>
3538               <property name="expand">False</property>
3539               <property name="fill">False</property>
3540             </packing>
3541           </child>
3542         </widget>
3543         <packing>
3544           <property name="left_attach">0</property>
3545           <property name="right_attach">2</property>
3546           <property name="top_attach">2</property>
3547           <property name="bottom_attach">3</property>
3548           <property name="y_padding">5</property>
3549         </packing>
3550       </child>
3551     </widget>
3552   </child>
3553 </widget>
3554
3555 <widget class="GtkWindow" id="NewDevelWin">
3556   <property name="title" translatable="yes">Create development</property>
3557   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3558   <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
3559   <property name="modal">True</property>
3560   <property name="resizable">False</property>
3561   <property name="destroy_with_parent">False</property>
3562   <property name="decorated">True</property>
3563   <property name="skip_taskbar_hint">False</property>
3564   <property name="skip_pager_hint">False</property>
3565   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
3566   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3567   <property name="focus_on_map">True</property>
3568   <property name="urgency_hint">False</property>
3569
3570   <child>
3571     <widget class="GtkVBox" id="vbox10">
3572       <property name="visible">True</property>
3573       <property name="homogeneous">False</property>
3574       <property name="spacing">0</property>
3575
3576       <child>
3577         <widget class="GtkTable" id="table2">
3578           <property name="border_width">3</property>
3579           <property name="visible">True</property>
3580           <property name="n_rows">2</property>
3581           <property name="n_columns">3</property>
3582           <property name="homogeneous">False</property>
3583           <property name="row_spacing">5</property>
3584           <property name="column_spacing">5</property>
3585
3586           <child>
3587             <widget class="GtkLabel" id="label20">
3588               <property name="visible">True</property>
3589               <property name="label" translatable="yes">Name</property>
3590               <property name="use_underline">False</property>
3591               <property name="use_markup">False</property>
3592               <property name="justify">GTK_JUSTIFY_LEFT</property>
3593               <property name="wrap">False</property>
3594               <property name="selectable">False</property>
3595               <property name="xalign">0</property>
3596               <property name="yalign">0.5</property>
3597               <property name="xpad">0</property>
3598               <property name="ypad">0</property>
3599               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3600               <property name="width_chars">-1</property>
3601               <property name="single_line_mode">False</property>
3602               <property name="angle">0</property>
3603             </widget>
3604             <packing>
3605               <property name="left_attach">0</property>
3606               <property name="right_attach">1</property>
3607               <property name="top_attach">0</property>
3608               <property name="bottom_attach">1</property>
3609               <property name="x_options">fill</property>
3610               <property name="y_options"></property>
3611             </packing>
3612           </child>
3613
3614           <child>
3615             <widget class="GtkLabel" id="label21">
3616               <property name="visible">True</property>
3617               <property name="label" translatable="yes">Root directory</property>
3618               <property name="use_underline">False</property>
3619               <property name="use_markup">False</property>
3620               <property name="justify">GTK_JUSTIFY_LEFT</property>
3621               <property name="wrap">False</property>
3622               <property name="selectable">False</property>
3623               <property name="xalign">0</property>
3624               <property name="yalign">0.5</property>
3625               <property name="xpad">0</property>
3626               <property name="ypad">0</property>
3627               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3628               <property name="width_chars">-1</property>
3629               <property name="single_line_mode">False</property>
3630               <property name="angle">0</property>
3631             </widget>
3632             <packing>
3633               <property name="left_attach">0</property>
3634               <property name="right_attach">1</property>
3635               <property name="top_attach">1</property>
3636               <property name="bottom_attach">2</property>
3637               <property name="x_options">fill</property>
3638               <property name="y_options"></property>
3639             </packing>
3640           </child>
3641
3642           <child>
3643             <widget class="GtkEntry" id="nameEntry">
3644               <property name="visible">True</property>
3645               <property name="can_focus">True</property>
3646               <property name="editable">True</property>
3647               <property name="visibility">True</property>
3648               <property name="max_length">0</property>
3649               <property name="text" translatable="yes"></property>
3650               <property name="has_frame">True</property>
3651               <property name="invisible_char">*</property>
3652               <property name="activates_default">False</property>
3653             </widget>
3654             <packing>
3655               <property name="left_attach">1</property>
3656               <property name="right_attach">2</property>
3657               <property name="top_attach">0</property>
3658               <property name="bottom_attach">1</property>
3659               <property name="y_options"></property>
3660             </packing>
3661           </child>
3662
3663           <child>
3664             <widget class="GtkEntry" id="rootEntry">
3665               <property name="visible">True</property>
3666               <property name="can_focus">True</property>
3667               <property name="editable">True</property>
3668               <property name="visibility">True</property>
3669               <property name="max_length">0</property>
3670               <property name="text" translatable="yes"></property>
3671               <property name="has_frame">True</property>
3672               <property name="invisible_char">*</property>
3673               <property name="activates_default">False</property>
3674             </widget>
3675             <packing>
3676               <property name="left_attach">1</property>
3677               <property name="right_attach">2</property>
3678               <property name="top_attach">1</property>
3679               <property name="bottom_attach">2</property>
3680               <property name="y_options"></property>
3681             </packing>
3682           </child>
3683
3684           <child>
3685             <widget class="GtkButton" id="chooseRootButton">
3686               <property name="visible">True</property>
3687               <property name="can_focus">True</property>
3688               <property name="label" translatable="yes">...</property>
3689               <property name="use_underline">True</property>
3690               <property name="relief">GTK_RELIEF_NORMAL</property>
3691               <property name="focus_on_click">True</property>
3692             </widget>
3693             <packing>
3694               <property name="left_attach">2</property>
3695               <property name="right_attach">3</property>
3696               <property name="top_attach">1</property>
3697               <property name="bottom_attach">2</property>
3698               <property name="x_options">fill</property>
3699               <property name="y_options"></property>
3700             </packing>
3701           </child>
3702         </widget>
3703         <packing>
3704           <property name="padding">0</property>
3705           <property name="expand">False</property>
3706           <property name="fill">True</property>
3707         </packing>
3708       </child>
3709
3710       <child>
3711         <widget class="GtkHSeparator" id="hseparator1">
3712           <property name="visible">True</property>
3713         </widget>
3714         <packing>
3715           <property name="padding">2</property>
3716           <property name="expand">False</property>
3717           <property name="fill">True</property>
3718         </packing>
3719       </child>
3720
3721       <child>
3722         <widget class="GtkHBox" id="hbox21">
3723           <property name="border_width">3</property>
3724           <property name="visible">True</property>
3725           <property name="homogeneous">False</property>
3726           <property name="spacing">5</property>
3727
3728           <child>
3729             <widget class="GtkVBox" id="vbox11">
3730               <property name="visible">True</property>
3731               <property name="homogeneous">False</property>
3732               <property name="spacing">0</property>
3733
3734               <child>
3735                 <placeholder/>
3736               </child>
3737
3738               <child>
3739                 <placeholder/>
3740               </child>
3741             </widget>
3742             <packing>
3743               <property name="padding">0</property>
3744               <property name="expand">True</property>
3745               <property name="fill">True</property>
3746             </packing>
3747           </child>
3748
3749           <child>
3750             <widget class="GtkButton" id="addButton">
3751               <property name="visible">True</property>
3752               <property name="can_focus">True</property>
3753               <property name="label">gtk-add</property>
3754               <property name="use_stock">True</property>
3755               <property name="relief">GTK_RELIEF_NORMAL</property>
3756               <property name="focus_on_click">True</property>
3757             </widget>
3758             <packing>
3759               <property name="padding">0</property>
3760               <property name="expand">False</property>
3761               <property name="fill">False</property>
3762             </packing>
3763           </child>
3764
3765           <child>
3766             <widget class="GtkButton" id="cancelButton">
3767               <property name="visible">True</property>
3768               <property name="can_focus">True</property>
3769               <property name="label">gtk-cancel</property>
3770               <property name="use_stock">True</property>
3771               <property name="relief">GTK_RELIEF_NORMAL</property>
3772               <property name="focus_on_click">True</property>
3773             </widget>
3774             <packing>
3775               <property name="padding">0</property>
3776               <property name="expand">False</property>
3777               <property name="fill">False</property>
3778             </packing>
3779           </child>
3780         </widget>
3781         <packing>
3782           <property name="padding">0</property>
3783           <property name="expand">False</property>
3784           <property name="fill">True</property>
3785         </packing>
3786       </child>
3787     </widget>
3788   </child>
3789 </widget>
3790
3791 <widget class="GtkWindow" id="DevelListWin">
3792   <property name="title" translatable="yes">Developments</property>
3793   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3794   <property name="window_position">GTK_WIN_POS_CENTER</property>
3795   <property name="modal">False</property>
3796   <property name="resizable">True</property>
3797   <property name="destroy_with_parent">False</property>
3798   <property name="decorated">True</property>
3799   <property name="skip_taskbar_hint">False</property>
3800   <property name="skip_pager_hint">False</property>
3801   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
3802   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3803   <property name="focus_on_map">True</property>
3804   <property name="urgency_hint">False</property>
3805
3806   <child>
3807     <widget class="GtkVBox" id="vbox12">
3808       <property name="visible">True</property>
3809       <property name="homogeneous">False</property>
3810       <property name="spacing">0</property>
3811
3812       <child>
3813         <widget class="GtkScrolledWindow" id="scrolledwindow10">
3814           <property name="visible">True</property>
3815           <property name="can_focus">True</property>
3816           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3817           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3818           <property name="shadow_type">GTK_SHADOW_IN</property>
3819           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3820
3821           <child>
3822             <widget class="GtkTreeView" id="developmentsTreeview">
3823               <property name="visible">True</property>
3824               <property name="can_focus">True</property>
3825               <property name="headers_visible">False</property>
3826               <property name="rules_hint">False</property>
3827               <property name="reorderable">False</property>
3828               <property name="enable_search">True</property>
3829               <property name="fixed_height_mode">False</property>
3830               <property name="hover_selection">False</property>
3831               <property name="hover_expand">False</property>
3832             </widget>
3833           </child>
3834         </widget>
3835         <packing>
3836           <property name="padding">0</property>
3837           <property name="expand">True</property>
3838           <property name="fill">True</property>
3839         </packing>
3840       </child>
3841
3842       <child>
3843         <widget class="GtkHSeparator" id="hseparator2">
3844           <property name="visible">True</property>
3845         </widget>
3846         <packing>
3847           <property name="padding">2</property>
3848           <property name="expand">False</property>
3849           <property name="fill">True</property>
3850         </packing>
3851       </child>
3852
3853       <child>
3854         <widget class="GtkHBox" id="buttonsHbox">
3855           <property name="border_width">3</property>
3856           <property name="visible">True</property>
3857           <property name="homogeneous">False</property>
3858           <property name="spacing">4</property>
3859
3860           <child>
3861             <widget class="GtkVBox" id="vbox13">
3862               <property name="visible">True</property>
3863               <property name="homogeneous">False</property>
3864               <property name="spacing">0</property>
3865
3866               <child>
3867                 <placeholder/>
3868               </child>
3869
3870               <child>
3871                 <placeholder/>
3872               </child>
3873             </widget>
3874             <packing>
3875               <property name="padding">0</property>
3876               <property name="expand">True</property>
3877               <property name="fill">True</property>
3878             </packing>
3879           </child>
3880
3881           <child>
3882             <widget class="GtkButton" id="newButton">
3883               <property name="visible">True</property>
3884               <property name="can_focus">True</property>
3885               <property name="label">gtk-new</property>
3886               <property name="use_stock">True</property>
3887               <property name="relief">GTK_RELIEF_NORMAL</property>
3888               <property name="focus_on_click">True</property>
3889             </widget>
3890             <packing>
3891               <property name="padding">0</property>
3892               <property name="expand">False</property>
3893               <property name="fill">False</property>
3894             </packing>
3895           </child>
3896
3897           <child>
3898             <widget class="GtkButton" id="deleteButton">
3899               <property name="visible">True</property>
3900               <property name="can_focus">True</property>
3901               <property name="label">gtk-delete</property>
3902               <property name="use_stock">True</property>
3903               <property name="relief">GTK_RELIEF_NORMAL</property>
3904               <property name="focus_on_click">True</property>
3905             </widget>
3906             <packing>
3907               <property name="padding">0</property>
3908               <property name="expand">False</property>
3909               <property name="fill">False</property>
3910             </packing>
3911           </child>
3912
3913           <child>
3914             <widget class="GtkButton" id="buildButton">
3915               <property name="visible">True</property>
3916               <property name="can_focus">True</property>
3917               <property name="relief">GTK_RELIEF_NORMAL</property>
3918               <property name="focus_on_click">True</property>
3919
3920               <child>
3921                 <widget class="GtkAlignment" id="alignment14">
3922                   <property name="visible">True</property>
3923                   <property name="xalign">0.5</property>
3924                   <property name="yalign">0.5</property>
3925                   <property name="xscale">0</property>
3926                   <property name="yscale">0</property>
3927                   <property name="top_padding">0</property>
3928                   <property name="bottom_padding">0</property>
3929                   <property name="left_padding">0</property>
3930                   <property name="right_padding">0</property>
3931
3932                   <child>
3933                     <widget class="GtkHBox" id="hbox23">
3934                       <property name="visible">True</property>
3935                       <property name="homogeneous">False</property>
3936                       <property name="spacing">2</property>
3937
3938                       <child>
3939                         <widget class="GtkImage" id="image358">
3940                           <property name="visible">True</property>
3941                           <property name="stock">gtk-execute</property>
3942                           <property name="icon_size">4</property>
3943                           <property name="xalign">0.5</property>
3944                           <property name="yalign">0.5</property>
3945                           <property name="xpad">0</property>
3946                           <property name="ypad">0</property>
3947                         </widget>
3948                         <packing>
3949                           <property name="padding">0</property>
3950                           <property name="expand">False</property>
3951                           <property name="fill">False</property>
3952                         </packing>
3953                       </child>
3954
3955                       <child>
3956                         <widget class="GtkLabel" id="label22">
3957                           <property name="visible">True</property>
3958                           <property name="label" translatable="yes">_Build</property>
3959                           <property name="use_underline">True</property>
3960                           <property name="use_markup">False</property>
3961                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3962                           <property name="wrap">False</property>
3963                           <property name="selectable">False</property>
3964                           <property name="xalign">0.5</property>
3965                           <property name="yalign">0.5</property>
3966                           <property name="xpad">0</property>
3967                           <property name="ypad">0</property>
3968                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3969                           <property name="width_chars">-1</property>
3970                           <property name="single_line_mode">False</property>
3971                           <property name="angle">0</property>
3972                         </widget>
3973                         <packing>
3974                           <property name="padding">0</property>
3975                           <property name="expand">False</property>
3976                           <property name="fill">False</property>
3977                         </packing>
3978                       </child>
3979                     </widget>
3980                   </child>
3981                 </widget>
3982               </child>
3983             </widget>
3984             <packing>
3985               <property name="padding">0</property>
3986               <property name="expand">False</property>
3987               <property name="fill">False</property>
3988             </packing>
3989           </child>
3990
3991           <child>
3992             <widget class="GtkButton" id="cleanButton">
3993               <property name="visible">True</property>
3994               <property name="can_focus">True</property>
3995               <property name="relief">GTK_RELIEF_NORMAL</property>
3996               <property name="focus_on_click">True</property>
3997
3998               <child>
3999                 <widget class="GtkAlignment" id="alignment15">
4000                   <property name="visible">True</property>
4001                   <property name="xalign">0.5</property>
4002                   <property name="yalign">0.5</property>
4003                   <property name="xscale">0</property>
4004                   <property name="yscale">0</property>
4005                   <property name="top_padding">0</property>
4006                   <property name="bottom_padding">0</property>
4007                   <property name="left_padding">0</property>
4008                   <property name="right_padding">0</property>
4009
4010                   <child>
4011                     <widget class="GtkHBox" id="hbox24">
4012                       <property name="visible">True</property>
4013                       <property name="homogeneous">False</property>
4014                       <property name="spacing">2</property>
4015
4016                       <child>
4017                         <widget class="GtkImage" id="image359">
4018                           <property name="visible">True</property>
4019                           <property name="stock">gtk-clear</property>
4020                           <property name="icon_size">4</property>
4021                           <property name="xalign">0.5</property>
4022                           <property name="yalign">0.5</property>
4023                           <property name="xpad">0</property>
4024                           <property name="ypad">0</property>
4025                         </widget>
4026                         <packing>
4027                           <property name="padding">0</property>
4028                           <property name="expand">False</property>
4029                           <property name="fill">False</property>
4030                         </packing>
4031                       </child>
4032
4033                       <child>
4034                         <widget class="GtkLabel" id="label23">
4035                           <property name="visible">True</property>
4036                           <property name="label" translatable="yes">C_lean</property>
4037                           <property name="use_underline">True</property>
4038                           <property name="use_markup">False</property>
4039                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4040                           <property name="wrap">False</property>
4041                           <property name="selectable">False</property>
4042                           <property name="xalign">0.5</property>
4043                           <property name="yalign">0.5</property>
4044                           <property name="xpad">0</property>
4045                           <property name="ypad">0</property>
4046                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4047                           <property name="width_chars">-1</property>
4048                           <property name="single_line_mode">False</property>
4049                           <property name="angle">0</property>
4050                         </widget>
4051                         <packing>
4052                           <property name="padding">0</property>
4053                           <property name="expand">False</property>
4054                           <property name="fill">False</property>
4055                         </packing>
4056                       </child>
4057                     </widget>
4058                   </child>
4059                 </widget>
4060               </child>
4061             </widget>
4062             <packing>
4063               <property name="padding">0</property>
4064               <property name="expand">False</property>
4065               <property name="fill">False</property>
4066             </packing>
4067           </child>
4068
4069           <child>
4070             <widget class="GtkButton" id="publishButton">
4071               <property name="visible">True</property>
4072               <property name="can_focus">True</property>
4073               <property name="relief">GTK_RELIEF_NORMAL</property>
4074               <property name="focus_on_click">True</property>
4075
4076               <child>
4077                 <widget class="GtkAlignment" id="alignment16">
4078                   <property name="visible">True</property>
4079                   <property name="xalign">0.5</property>
4080                   <property name="yalign">0.5</property>
4081                   <property name="xscale">0</property>
4082                   <property name="yscale">0</property>
4083                   <property name="top_padding">0</property>
4084                   <property name="bottom_padding">0</property>
4085                   <property name="left_padding">0</property>
4086                   <property name="right_padding">0</property>
4087
4088                   <child>
4089                     <widget class="GtkHBox" id="hbox25">
4090                       <property name="visible">True</property>
4091                       <property name="homogeneous">False</property>
4092                       <property name="spacing">2</property>
4093
4094                       <child>
4095                         <widget class="GtkImage" id="image907">
4096                           <property name="visible">True</property>
4097                           <property name="stock">gtk-convert</property>
4098                           <property name="icon_size">4</property>
4099                           <property name="xalign">0.5</property>
4100                           <property name="yalign">0.5</property>
4101                           <property name="xpad">0</property>
4102                           <property name="ypad">0</property>
4103                         </widget>
4104                         <packing>
4105                           <property name="padding">0</property>
4106                           <property name="expand">False</property>
4107                           <property name="fill">False</property>
4108                         </packing>
4109                       </child>
4110
4111                       <child>
4112                         <widget class="GtkLabel" id="label24">
4113                           <property name="visible">True</property>
4114                           <property name="label" translatable="yes">Publish</property>
4115                           <property name="use_underline">True</property>
4116                           <property name="use_markup">False</property>
4117                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4118                           <property name="wrap">False</property>
4119                           <property name="selectable">False</property>
4120                           <property name="xalign">0.5</property>
4121                           <property name="yalign">0.5</property>
4122                           <property name="xpad">0</property>
4123                           <property name="ypad">0</property>
4124                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4125                           <property name="width_chars">-1</property>
4126                           <property name="single_line_mode">False</property>
4127                           <property name="angle">0</property>
4128                         </widget>
4129                         <packing>
4130                           <property name="padding">0</property>
4131                           <property name="expand">False</property>
4132                           <property name="fill">False</property>
4133                         </packing>
4134                       </child>
4135                     </widget>
4136                   </child>
4137                 </widget>
4138               </child>
4139             </widget>
4140             <packing>
4141               <property name="padding">0</property>
4142               <property name="expand">False</property>
4143               <property name="fill">False</property>
4144             </packing>
4145           </child>
4146
4147           <child>
4148             <widget class="GtkButton" id="graphButton">
4149               <property name="visible">True</property>
4150               <property name="can_focus">True</property>
4151               <property name="relief">GTK_RELIEF_NORMAL</property>
4152               <property name="focus_on_click">True</property>
4153
4154               <child>
4155                 <widget class="GtkAlignment" id="alignment17">
4156                   <property name="visible">True</property>
4157                   <property name="xalign">0.5</property>
4158                   <property name="yalign">0.5</property>
4159                   <property name="xscale">0</property>
4160                   <property name="yscale">0</property>
4161                   <property name="top_padding">0</property>
4162                   <property name="bottom_padding">0</property>
4163                   <property name="left_padding">0</property>
4164                   <property name="right_padding">0</property>
4165
4166                   <child>
4167                     <widget class="GtkHBox" id="hbox26">
4168                       <property name="visible">True</property>
4169                       <property name="homogeneous">False</property>
4170                       <property name="spacing">2</property>
4171
4172                       <child>
4173                         <widget class="GtkImage" id="image908">
4174                           <property name="visible">True</property>
4175                           <property name="stock">gtk-zoom-fit</property>
4176                           <property name="icon_size">4</property>
4177                           <property name="xalign">0.5</property>
4178                           <property name="yalign">0.5</property>
4179                           <property name="xpad">0</property>
4180                           <property name="ypad">0</property>
4181                         </widget>
4182                         <packing>
4183                           <property name="padding">0</property>
4184                           <property name="expand">False</property>
4185                           <property name="fill">False</property>
4186                         </packing>
4187                       </child>
4188
4189                       <child>
4190                         <widget class="GtkLabel" id="label27">
4191                           <property name="visible">True</property>
4192                           <property name="label" translatable="yes">Graph</property>
4193                           <property name="use_underline">True</property>
4194                           <property name="use_markup">False</property>
4195                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4196                           <property name="wrap">False</property>
4197                           <property name="selectable">False</property>
4198                           <property name="xalign">0.5</property>
4199                           <property name="yalign">0.5</property>
4200                           <property name="xpad">0</property>
4201                           <property name="ypad">0</property>
4202                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4203                           <property name="width_chars">-1</property>
4204                           <property name="single_line_mode">False</property>
4205                           <property name="angle">0</property>
4206                         </widget>
4207                         <packing>
4208                           <property name="padding">0</property>
4209                           <property name="expand">False</property>
4210                           <property name="fill">False</property>
4211                         </packing>
4212                       </child>
4213                     </widget>
4214                   </child>
4215                 </widget>
4216               </child>
4217             </widget>
4218             <packing>
4219               <property name="padding">0</property>
4220               <property name="expand">False</property>
4221               <property name="fill">False</property>
4222             </packing>
4223           </child>
4224
4225           <child>
4226             <widget class="GtkButton" id="closeButton">
4227               <property name="visible">True</property>
4228               <property name="can_focus">True</property>
4229               <property name="label">gtk-close</property>
4230               <property name="use_stock">True</property>
4231               <property name="relief">GTK_RELIEF_NORMAL</property>
4232               <property name="focus_on_click">True</property>
4233             </widget>
4234             <packing>
4235               <property name="padding">0</property>
4236               <property name="expand">False</property>
4237               <property name="fill">False</property>
4238             </packing>
4239           </child>
4240         </widget>
4241         <packing>
4242           <property name="padding">0</property>
4243           <property name="expand">False</property>
4244           <property name="fill">True</property>
4245         </packing>
4246       </child>
4247     </widget>
4248   </child>
4249 </widget>
4250
4251 <widget class="GtkWindow" id="window1">
4252   <property name="visible">True</property>
4253   <property name="title" translatable="yes">window1</property>
4254   <property name="type">GTK_WINDOW_TOPLEVEL</property>
4255   <property name="window_position">GTK_WIN_POS_NONE</property>
4256   <property name="modal">False</property>
4257   <property name="resizable">True</property>
4258   <property name="destroy_with_parent">False</property>
4259   <property name="decorated">True</property>
4260   <property name="skip_taskbar_hint">False</property>
4261   <property name="skip_pager_hint">False</property>
4262   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
4263   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
4264   <property name="focus_on_map">True</property>
4265   <property name="urgency_hint">False</property>
4266
4267   <child>
4268     <widget class="GtkHBox" id="hbox27">
4269       <property name="visible">True</property>
4270       <property name="homogeneous">False</property>
4271       <property name="spacing">0</property>
4272
4273       <child>
4274         <widget class="GtkToolbar" id="toolbar1">
4275           <property name="visible">True</property>
4276           <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
4277           <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
4278           <property name="tooltips">True</property>
4279           <property name="show_arrow">True</property>
4280
4281           <child>
4282             <widget class="GtkToolItem" id="toolitem30">
4283               <property name="visible">True</property>
4284               <property name="visible_horizontal">True</property>
4285               <property name="visible_vertical">True</property>
4286               <property name="is_important">False</property>
4287
4288               <child>
4289                 <widget class="GtkButton" id="button1">
4290                   <property name="visible">True</property>
4291                   <property name="tooltip" translatable="yes">Restart</property>
4292                   <property name="can_focus">True</property>
4293                   <property name="relief">GTK_RELIEF_NONE</property>
4294                   <property name="focus_on_click">True</property>
4295
4296                   <child>
4297                     <widget class="GtkImage" id="image909">
4298                       <property name="visible">True</property>
4299                       <property name="stock">gtk-goto-top</property>
4300                       <property name="icon_size">4</property>
4301                       <property name="xalign">0.5</property>
4302                       <property name="yalign">0.5</property>
4303                       <property name="xpad">0</property>
4304                       <property name="ypad">0</property>
4305                     </widget>
4306                   </child>
4307                 </widget>
4308               </child>
4309             </widget>
4310             <packing>
4311               <property name="expand">False</property>
4312               <property name="homogeneous">False</property>
4313             </packing>
4314           </child>
4315
4316           <child>
4317             <widget class="GtkToolItem" id="toolitem31">
4318               <property name="visible">True</property>
4319               <property name="visible_horizontal">True</property>
4320               <property name="visible_vertical">True</property>
4321               <property name="is_important">False</property>
4322
4323               <child>
4324                 <widget class="GtkButton" id="button2">
4325                   <property name="visible">True</property>
4326                   <property name="tooltip" translatable="yes">Retract 1 phrase</property>
4327                   <property name="can_focus">True</property>
4328                   <property name="relief">GTK_RELIEF_NONE</property>
4329                   <property name="focus_on_click">True</property>
4330
4331                   <child>
4332                     <widget class="GtkImage" id="image910">
4333                       <property name="visible">True</property>
4334                       <property name="stock">gtk-go-up</property>
4335                       <property name="icon_size">4</property>
4336                       <property name="xalign">0.5</property>
4337                       <property name="yalign">0.5</property>
4338                       <property name="xpad">0</property>
4339                       <property name="ypad">0</property>
4340                     </widget>
4341                   </child>
4342                 </widget>
4343               </child>
4344             </widget>
4345             <packing>
4346               <property name="expand">False</property>
4347               <property name="homogeneous">False</property>
4348             </packing>
4349           </child>
4350
4351           <child>
4352             <widget class="GtkToolItem" id="toolitem32">
4353               <property name="visible">True</property>
4354               <property name="visible_horizontal">True</property>
4355               <property name="visible_vertical">True</property>
4356               <property name="is_important">False</property>
4357
4358               <child>
4359                 <widget class="GtkButton" id="button3">
4360                   <property name="visible">True</property>
4361                   <property name="tooltip" translatable="yes">Execute until point</property>
4362                   <property name="can_focus">True</property>
4363                   <property name="relief">GTK_RELIEF_NONE</property>
4364                   <property name="focus_on_click">True</property>
4365
4366                   <child>
4367                     <widget class="GtkImage" id="image911">
4368                       <property name="visible">True</property>
4369                       <property name="stock">gtk-jump-to</property>
4370                       <property name="icon_size">4</property>
4371                       <property name="xalign">0.5</property>
4372                       <property name="yalign">0.5</property>
4373                       <property name="xpad">0</property>
4374                       <property name="ypad">0</property>
4375                     </widget>
4376                   </child>
4377                 </widget>
4378               </child>
4379             </widget>
4380             <packing>
4381               <property name="expand">False</property>
4382               <property name="homogeneous">False</property>
4383             </packing>
4384           </child>
4385
4386           <child>
4387             <widget class="GtkToolItem" id="toolitem33">
4388               <property name="visible">True</property>
4389               <property name="visible_horizontal">True</property>
4390               <property name="visible_vertical">True</property>
4391               <property name="is_important">False</property>
4392
4393               <child>
4394                 <widget class="GtkButton" id="button4">
4395                   <property name="visible">True</property>
4396                   <property name="tooltip" translatable="yes">Execute 1 phrase</property>
4397                   <property name="can_focus">True</property>
4398                   <property name="relief">GTK_RELIEF_NONE</property>
4399                   <property name="focus_on_click">True</property>
4400
4401                   <child>
4402                     <widget class="GtkImage" id="image912">
4403                       <property name="visible">True</property>
4404                       <property name="stock">gtk-go-down</property>
4405                       <property name="icon_size">4</property>
4406                       <property name="xalign">0.5</property>
4407                       <property name="yalign">0.5</property>
4408                       <property name="xpad">0</property>
4409                       <property name="ypad">0</property>
4410                     </widget>
4411                   </child>
4412                 </widget>
4413               </child>
4414             </widget>
4415             <packing>
4416               <property name="expand">False</property>
4417               <property name="homogeneous">False</property>
4418             </packing>
4419           </child>
4420
4421           <child>
4422             <widget class="GtkToolItem" id="toolitem34">
4423               <property name="visible">True</property>
4424               <property name="visible_horizontal">True</property>
4425               <property name="visible_vertical">True</property>
4426               <property name="is_important">False</property>
4427
4428               <child>
4429                 <widget class="GtkButton" id="button5">
4430                   <property name="visible">True</property>
4431                   <property name="tooltip" translatable="yes">Execute all</property>
4432                   <property name="can_focus">True</property>
4433                   <property name="relief">GTK_RELIEF_NONE</property>
4434                   <property name="focus_on_click">True</property>
4435
4436                   <child>
4437                     <widget class="GtkImage" id="image913">
4438                       <property name="visible">True</property>
4439                       <property name="stock">gtk-goto-bottom</property>
4440                       <property name="icon_size">4</property>
4441                       <property name="xalign">0.5</property>
4442                       <property name="yalign">0.5</property>
4443                       <property name="xpad">0</property>
4444                       <property name="ypad">0</property>
4445                     </widget>
4446                   </child>
4447                 </widget>
4448               </child>
4449             </widget>
4450             <packing>
4451               <property name="expand">False</property>
4452               <property name="homogeneous">False</property>
4453             </packing>
4454           </child>
4455         </widget>
4456         <packing>
4457           <property name="padding">0</property>
4458           <property name="expand">True</property>
4459           <property name="fill">True</property>
4460         </packing>
4461       </child>
4462
4463       <child>
4464         <widget class="GtkImage" id="image914">
4465           <property name="visible">True</property>
4466           <property name="stock">gtk-cancel</property>
4467           <property name="icon_size">4</property>
4468           <property name="xalign">0.5</property>
4469           <property name="yalign">0.5</property>
4470           <property name="xpad">0</property>
4471           <property name="ypad">0</property>
4472         </widget>
4473         <packing>
4474           <property name="padding">0</property>
4475           <property name="expand">False</property>
4476           <property name="fill">False</property>
4477         </packing>
4478       </child>
4479     </widget>
4480   </child>
4481 </widget>
4482
4483 <widget class="GtkDialog" id="DisambiguationErrors">
4484   <property name="width_request">450</property>
4485   <property name="height_request">400</property>
4486   <property name="title" translatable="yes">title</property>
4487   <property name="type">GTK_WINDOW_TOPLEVEL</property>
4488   <property name="window_position">GTK_WIN_POS_NONE</property>
4489   <property name="modal">True</property>
4490   <property name="resizable">True</property>
4491   <property name="destroy_with_parent">False</property>
4492   <property name="decorated">True</property>
4493   <property name="skip_taskbar_hint">False</property>
4494   <property name="skip_pager_hint">False</property>
4495   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
4496   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
4497   <property name="focus_on_map">True</property>
4498   <property name="urgency_hint">False</property>
4499   <property name="has_separator">True</property>
4500
4501   <child internal-child="vbox">
4502     <widget class="GtkVBox" id="vbox14">
4503       <property name="visible">True</property>
4504       <property name="homogeneous">False</property>
4505       <property name="spacing">0</property>
4506
4507       <child internal-child="action_area">
4508         <widget class="GtkHButtonBox" id="hbuttonbox2">
4509           <property name="visible">True</property>
4510           <property name="layout_style">GTK_BUTTONBOX_END</property>
4511
4512           <child>
4513             <widget class="GtkButton" id="button6">
4514               <property name="visible">True</property>
4515               <property name="can_default">True</property>
4516               <property name="can_focus">True</property>
4517               <property name="label">gtk-help</property>
4518               <property name="use_stock">True</property>
4519               <property name="relief">GTK_RELIEF_NORMAL</property>
4520               <property name="focus_on_click">True</property>
4521               <property name="response_id">-11</property>
4522             </widget>
4523           </child>
4524
4525           <child>
4526             <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
4527               <property name="visible">True</property>
4528               <property name="can_default">True</property>
4529               <property name="can_focus">True</property>
4530               <property name="relief">GTK_RELIEF_NORMAL</property>
4531               <property name="focus_on_click">True</property>
4532               <property name="response_id">-6</property>
4533
4534               <child>
4535                 <widget class="GtkAlignment" id="alignment18">
4536                   <property name="visible">True</property>
4537                   <property name="xalign">0.5</property>
4538                   <property name="yalign">0.5</property>
4539                   <property name="xscale">0</property>
4540                   <property name="yscale">0</property>
4541                   <property name="top_padding">0</property>
4542                   <property name="bottom_padding">0</property>
4543                   <property name="left_padding">0</property>
4544                   <property name="right_padding">0</property>
4545
4546                   <child>
4547                     <widget class="GtkHBox" id="hbox29">
4548                       <property name="visible">True</property>
4549                       <property name="homogeneous">False</property>
4550                       <property name="spacing">2</property>
4551
4552                       <child>
4553                         <widget class="GtkImage" id="image926">
4554                           <property name="visible">True</property>
4555                           <property name="stock">gtk-zoom-in</property>
4556                           <property name="icon_size">4</property>
4557                           <property name="xalign">0.5</property>
4558                           <property name="yalign">0.5</property>
4559                           <property name="xpad">0</property>
4560                           <property name="ypad">0</property>
4561                         </widget>
4562                         <packing>
4563                           <property name="padding">0</property>
4564                           <property name="expand">False</property>
4565                           <property name="fill">False</property>
4566                         </packing>
4567                       </child>
4568
4569                       <child>
4570                         <widget class="GtkLabel" id="label28">
4571                           <property name="visible">True</property>
4572                           <property name="label">More</property>
4573                           <property name="use_underline">True</property>
4574                           <property name="use_markup">False</property>
4575                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4576                           <property name="wrap">False</property>
4577                           <property name="selectable">False</property>
4578                           <property name="xalign">0.5</property>
4579                           <property name="yalign">0.5</property>
4580                           <property name="xpad">0</property>
4581                           <property name="ypad">0</property>
4582                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4583                           <property name="width_chars">-1</property>
4584                           <property name="single_line_mode">False</property>
4585                           <property name="angle">0</property>
4586                         </widget>
4587                         <packing>
4588                           <property name="padding">0</property>
4589                           <property name="expand">False</property>
4590                           <property name="fill">False</property>
4591                         </packing>
4592                       </child>
4593                     </widget>
4594                   </child>
4595                 </widget>
4596               </child>
4597             </widget>
4598           </child>
4599
4600           <child>
4601             <widget class="GtkButton" id="disambiguationErrorsCancelButton">
4602               <property name="visible">True</property>
4603               <property name="can_default">True</property>
4604               <property name="has_default">True</property>
4605               <property name="can_focus">True</property>
4606               <property name="label">gtk-cancel</property>
4607               <property name="use_stock">True</property>
4608               <property name="relief">GTK_RELIEF_NORMAL</property>
4609               <property name="focus_on_click">True</property>
4610               <property name="response_id">-6</property>
4611             </widget>
4612           </child>
4613
4614           <child>
4615             <widget class="GtkButton" id="disambiguationErrorsOkButton">
4616               <property name="visible">True</property>
4617               <property name="can_default">True</property>
4618               <property name="can_focus">True</property>
4619               <property name="label">gtk-ok</property>
4620               <property name="use_stock">True</property>
4621               <property name="relief">GTK_RELIEF_NORMAL</property>
4622               <property name="focus_on_click">True</property>
4623               <property name="response_id">-5</property>
4624             </widget>
4625           </child>
4626         </widget>
4627         <packing>
4628           <property name="padding">0</property>
4629           <property name="expand">False</property>
4630           <property name="fill">True</property>
4631           <property name="pack_type">GTK_PACK_END</property>
4632         </packing>
4633       </child>
4634
4635       <child>
4636         <widget class="GtkVBox" id="vbox15">
4637           <property name="visible">True</property>
4638           <property name="homogeneous">False</property>
4639           <property name="spacing">0</property>
4640
4641           <child>
4642             <widget class="GtkLabel" id="disambiguationErrorsLabel">
4643               <property name="visible">True</property>
4644               <property name="label" translatable="yes">some informative message here ...</property>
4645               <property name="use_underline">False</property>
4646               <property name="use_markup">False</property>
4647               <property name="justify">GTK_JUSTIFY_LEFT</property>
4648               <property name="wrap">False</property>
4649               <property name="selectable">False</property>
4650               <property name="xalign">0.5</property>
4651               <property name="yalign">0.5</property>
4652               <property name="xpad">0</property>
4653               <property name="ypad">0</property>
4654               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4655               <property name="width_chars">-1</property>
4656               <property name="single_line_mode">False</property>
4657               <property name="angle">0</property>
4658             </widget>
4659             <packing>
4660               <property name="padding">0</property>
4661               <property name="expand">False</property>
4662               <property name="fill">False</property>
4663             </packing>
4664           </child>
4665
4666           <child>
4667             <widget class="GtkScrolledWindow" id="scrolledwindow12">
4668               <property name="visible">True</property>
4669               <property name="can_focus">True</property>
4670               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4671               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4672               <property name="shadow_type">GTK_SHADOW_IN</property>
4673               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
4674
4675               <child>
4676                 <widget class="GtkTreeView" id="treeview">
4677                   <property name="visible">True</property>
4678                   <property name="can_focus">True</property>
4679                   <property name="headers_visible">False</property>
4680                   <property name="rules_hint">False</property>
4681                   <property name="reorderable">False</property>
4682                   <property name="enable_search">True</property>
4683                   <property name="fixed_height_mode">False</property>
4684                   <property name="hover_selection">False</property>
4685                   <property name="hover_expand">False</property>
4686                 </widget>
4687               </child>
4688             </widget>
4689             <packing>
4690               <property name="padding">0</property>
4691               <property name="expand">True</property>
4692               <property name="fill">True</property>
4693             </packing>
4694           </child>
4695         </widget>
4696         <packing>
4697           <property name="padding">0</property>
4698           <property name="expand">True</property>
4699           <property name="fill">True</property>
4700         </packing>
4701       </child>
4702     </widget>
4703   </child>
4704 </widget>
4705
4706 </glade-interface>