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