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="image979">
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="image980">
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="image981">
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="image982">
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="image983">
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="image984">
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="image985">
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="image986">
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="image987">
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="image988">
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="image989">
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="image990">
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="image991">
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="image992">
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="image993">
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="image994">
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="formulaePpMenuItem">
1621                               <property name="visible">True</property>
1622                               <property name="label" translatable="yes">Pretty print formulae</property>
1623                               <property name="use_underline">True</property>
1624                               <property name="active">True</property>
1625                               <accelerator key="p" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1626                             </widget>
1627                           </child>
1628                         </widget>
1629                       </child>
1630                     </widget>
1631                   </child>
1632
1633                   <child>
1634                     <widget class="GtkMenuItem" id="debugMenu">
1635                       <property name="visible">True</property>
1636                       <property name="label" translatable="yes">_Debug</property>
1637                       <property name="use_underline">True</property>
1638
1639                       <child>
1640                         <widget class="GtkMenu" id="debugMenu_menu">
1641
1642                           <child>
1643                             <widget class="GtkSeparatorMenuItem" id="separator6">
1644                               <property name="visible">True</property>
1645                             </widget>
1646                           </child>
1647                         </widget>
1648                       </child>
1649                     </widget>
1650                   </child>
1651
1652                   <child>
1653                     <widget class="GtkMenuItem" id="helpMenu">
1654                       <property name="visible">True</property>
1655                       <property name="label" translatable="yes">_Help</property>
1656                       <property name="use_underline">True</property>
1657
1658                       <child>
1659                         <widget class="GtkMenu" id="helpMenu_menu">
1660
1661                           <child>
1662                             <widget class="GtkImageMenuItem" id="contentsMenuItem">
1663                               <property name="visible">True</property>
1664                               <property name="label" translatable="yes">_Contents</property>
1665                               <property name="use_underline">True</property>
1666                               <accelerator key="F1" modifiers="0" signal="activate"/>
1667
1668                               <child internal-child="image">
1669                                 <widget class="GtkImage" id="image995">
1670                                   <property name="visible">True</property>
1671                                   <property name="stock">gtk-help</property>
1672                                   <property name="icon_size">1</property>
1673                                   <property name="xalign">0.5</property>
1674                                   <property name="yalign">0.5</property>
1675                                   <property name="xpad">0</property>
1676                                   <property name="ypad">0</property>
1677                                 </widget>
1678                               </child>
1679                             </widget>
1680                           </child>
1681
1682                           <child>
1683                             <widget class="GtkImageMenuItem" id="aboutMenuItem">
1684                               <property name="visible">True</property>
1685                               <property name="label" translatable="yes">_About</property>
1686                               <property name="use_underline">True</property>
1687
1688                               <child internal-child="image">
1689                                 <widget class="GtkImage" id="image996">
1690                                   <property name="visible">True</property>
1691                                   <property name="stock">gtk-about</property>
1692                                   <property name="icon_size">1</property>
1693                                   <property name="xalign">0.5</property>
1694                                   <property name="yalign">0.5</property>
1695                                   <property name="xpad">0</property>
1696                                   <property name="ypad">0</property>
1697                                 </widget>
1698                               </child>
1699                             </widget>
1700                           </child>
1701                         </widget>
1702                       </child>
1703                     </widget>
1704                   </child>
1705                 </widget>
1706               </child>
1707             </widget>
1708             <packing>
1709               <property name="padding">0</property>
1710               <property name="expand">False</property>
1711               <property name="fill">False</property>
1712             </packing>
1713           </child>
1714
1715           <child>
1716             <widget class="GtkHBox" id="hbox9">
1717               <property name="visible">True</property>
1718               <property name="homogeneous">False</property>
1719               <property name="spacing">0</property>
1720
1721               <child>
1722                 <widget class="GtkHPaned" id="hpaneScriptSequent">
1723                   <property name="visible">True</property>
1724                   <property name="can_focus">True</property>
1725
1726                   <child>
1727                     <widget class="GtkHBox" id="hbox18">
1728                       <property name="visible">True</property>
1729                       <property name="homogeneous">False</property>
1730                       <property name="spacing">0</property>
1731
1732                       <child>
1733                         <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1734                           <property name="visible">True</property>
1735                           <property name="shadow_type">GTK_SHADOW_OUT</property>
1736                           <property name="handle_position">GTK_POS_TOP</property>
1737                           <property name="snap_edge">GTK_POS_TOP</property>
1738
1739                           <child>
1740                             <widget class="GtkTable" id="ToolBarTable">
1741                               <property name="visible">True</property>
1742                               <property name="n_rows">17</property>
1743                               <property name="n_columns">2</property>
1744                               <property name="homogeneous">False</property>
1745                               <property name="row_spacing">4</property>
1746                               <property name="column_spacing">0</property>
1747
1748                               <child>
1749                                 <widget class="GtkButton" id="applyButton">
1750                                   <property name="visible">True</property>
1751                                   <property name="tooltip" translatable="yes">Apply</property>
1752                                   <property name="can_focus">True</property>
1753                                   <property name="label" translatable="yes">apply</property>
1754                                   <property name="use_underline">True</property>
1755                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1756                                   <property name="focus_on_click">True</property>
1757                                 </widget>
1758                                 <packing>
1759                                   <property name="left_attach">1</property>
1760                                   <property name="right_attach">2</property>
1761                                   <property name="top_attach">0</property>
1762                                   <property name="bottom_attach">1</property>
1763                                   <property name="x_options">fill</property>
1764                                   <property name="y_options"></property>
1765                                 </packing>
1766                               </child>
1767
1768                               <child>
1769                                 <widget class="GtkButton" id="introsButton">
1770                                   <property name="visible">True</property>
1771                                   <property name="tooltip" translatable="yes">Intros</property>
1772                                   <property name="can_focus">True</property>
1773                                   <property name="label" translatable="yes">intro</property>
1774                                   <property name="use_underline">True</property>
1775                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1776                                   <property name="focus_on_click">True</property>
1777                                 </widget>
1778                                 <packing>
1779                                   <property name="left_attach">0</property>
1780                                   <property name="right_attach">1</property>
1781                                   <property name="top_attach">0</property>
1782                                   <property name="bottom_attach">1</property>
1783                                   <property name="x_options">fill</property>
1784                                   <property name="y_options"></property>
1785                                 </packing>
1786                               </child>
1787
1788                               <child>
1789                                 <widget class="GtkButton" id="exactButton">
1790                                   <property name="visible">True</property>
1791                                   <property name="tooltip" translatable="yes">Exact</property>
1792                                   <property name="can_focus">True</property>
1793                                   <property name="label" translatable="yes">exact</property>
1794                                   <property name="use_underline">True</property>
1795                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1796                                   <property name="focus_on_click">True</property>
1797                                 </widget>
1798                                 <packing>
1799                                   <property name="left_attach">0</property>
1800                                   <property name="right_attach">1</property>
1801                                   <property name="top_attach">2</property>
1802                                   <property name="bottom_attach">3</property>
1803                                   <property name="x_options">fill</property>
1804                                   <property name="y_options"></property>
1805                                 </packing>
1806                               </child>
1807
1808                               <child>
1809                                 <widget class="GtkButton" id="elimButton">
1810                                   <property name="visible">True</property>
1811                                   <property name="tooltip" translatable="yes">Elim</property>
1812                                   <property name="can_focus">True</property>
1813                                   <property name="label" translatable="yes">elim</property>
1814                                   <property name="use_underline">True</property>
1815                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1816                                   <property name="focus_on_click">True</property>
1817                                 </widget>
1818                                 <packing>
1819                                   <property name="left_attach">0</property>
1820                                   <property name="right_attach">1</property>
1821                                   <property name="top_attach">4</property>
1822                                   <property name="bottom_attach">5</property>
1823                                   <property name="x_options">fill</property>
1824                                   <property name="y_options"></property>
1825                                 </packing>
1826                               </child>
1827
1828                               <child>
1829                                 <widget class="GtkButton" id="reflexivityButton">
1830                                   <property name="visible">True</property>
1831                                   <property name="tooltip" translatable="yes">Reflexivity</property>
1832                                   <property name="can_focus">True</property>
1833                                   <property name="label" translatable="yes">refl</property>
1834                                   <property name="use_underline">True</property>
1835                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1836                                   <property name="focus_on_click">True</property>
1837                                 </widget>
1838                                 <packing>
1839                                   <property name="left_attach">0</property>
1840                                   <property name="right_attach">1</property>
1841                                   <property name="top_attach">8</property>
1842                                   <property name="bottom_attach">9</property>
1843                                   <property name="x_options">fill</property>
1844                                   <property name="y_options"></property>
1845                                 </packing>
1846                               </child>
1847
1848                               <child>
1849                                 <widget class="GtkButton" id="symmetryButton">
1850                                   <property name="visible">True</property>
1851                                   <property name="tooltip" translatable="yes">Symmetry</property>
1852                                   <property name="can_focus">True</property>
1853                                   <property name="label" translatable="yes">sym</property>
1854                                   <property name="use_underline">True</property>
1855                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1856                                   <property name="focus_on_click">True</property>
1857                                 </widget>
1858                                 <packing>
1859                                   <property name="left_attach">1</property>
1860                                   <property name="right_attach">2</property>
1861                                   <property name="top_attach">8</property>
1862                                   <property name="bottom_attach">9</property>
1863                                   <property name="x_options">fill</property>
1864                                   <property name="y_options"></property>
1865                                 </packing>
1866                               </child>
1867
1868                               <child>
1869                                 <widget class="GtkButton" id="transitivityButton">
1870                                   <property name="visible">True</property>
1871                                   <property name="tooltip" translatable="yes">Transitivity</property>
1872                                   <property name="can_focus">True</property>
1873                                   <property name="label" translatable="yes">trans</property>
1874                                   <property name="use_underline">True</property>
1875                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1876                                   <property name="focus_on_click">True</property>
1877                                 </widget>
1878                                 <packing>
1879                                   <property name="left_attach">0</property>
1880                                   <property name="right_attach">1</property>
1881                                   <property name="top_attach">9</property>
1882                                   <property name="bottom_attach">10</property>
1883                                   <property name="x_options">fill</property>
1884                                   <property name="y_options"></property>
1885                                 </packing>
1886                               </child>
1887
1888                               <child>
1889                                 <widget class="GtkButton" id="simplifyButton">
1890                                   <property name="visible">True</property>
1891                                   <property name="tooltip" translatable="yes">Simplify</property>
1892                                   <property name="can_focus">True</property>
1893                                   <property name="label" translatable="yes">simpl</property>
1894                                   <property name="use_underline">True</property>
1895                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1896                                   <property name="focus_on_click">True</property>
1897                                 </widget>
1898                                 <packing>
1899                                   <property name="left_attach">0</property>
1900                                   <property name="right_attach">1</property>
1901                                   <property name="top_attach">11</property>
1902                                   <property name="bottom_attach">12</property>
1903                                   <property name="x_options">fill</property>
1904                                   <property name="y_options"></property>
1905                                 </packing>
1906                               </child>
1907
1908                               <child>
1909                                 <widget class="GtkButton" id="reduceButton">
1910                                   <property name="visible">True</property>
1911                                   <property name="tooltip" translatable="yes">Reduce</property>
1912                                   <property name="can_focus">True</property>
1913                                   <property name="label" translatable="yes">red</property>
1914                                   <property name="use_underline">True</property>
1915                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1916                                   <property name="focus_on_click">True</property>
1917                                 </widget>
1918                                 <packing>
1919                                   <property name="left_attach">1</property>
1920                                   <property name="right_attach">2</property>
1921                                   <property name="top_attach">11</property>
1922                                   <property name="bottom_attach">12</property>
1923                                   <property name="x_options">fill</property>
1924                                   <property name="y_options"></property>
1925                                 </packing>
1926                               </child>
1927
1928                               <child>
1929                                 <widget class="GtkButton" id="whdButton">
1930                                   <property name="visible">True</property>
1931                                   <property name="tooltip" translatable="yes">Whd</property>
1932                                   <property name="can_focus">True</property>
1933                                   <property name="label" translatable="yes">whd</property>
1934                                   <property name="use_underline">True</property>
1935                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1936                                   <property name="focus_on_click">True</property>
1937                                 </widget>
1938                                 <packing>
1939                                   <property name="left_attach">0</property>
1940                                   <property name="right_attach">1</property>
1941                                   <property name="top_attach">12</property>
1942                                   <property name="bottom_attach">13</property>
1943                                   <property name="x_options">fill</property>
1944                                   <property name="y_options"></property>
1945                                 </packing>
1946                               </child>
1947
1948                               <child>
1949                                 <widget class="GtkButton" id="assumptionButton">
1950                                   <property name="visible">True</property>
1951                                   <property name="tooltip" translatable="yes">Assumption</property>
1952                                   <property name="can_focus">True</property>
1953                                   <property name="label" translatable="yes">assum</property>
1954                                   <property name="use_underline">True</property>
1955                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1956                                   <property name="focus_on_click">True</property>
1957                                 </widget>
1958                                 <packing>
1959                                   <property name="left_attach">0</property>
1960                                   <property name="right_attach">1</property>
1961                                   <property name="top_attach">14</property>
1962                                   <property name="bottom_attach">15</property>
1963                                   <property name="x_options">fill</property>
1964                                   <property name="y_options"></property>
1965                                 </packing>
1966                               </child>
1967
1968                               <child>
1969                                 <widget class="GtkButton" id="autoButton">
1970                                   <property name="visible">True</property>
1971                                   <property name="tooltip" translatable="yes">Auto</property>
1972                                   <property name="can_focus">True</property>
1973                                   <property name="label" translatable="yes">auto</property>
1974                                   <property name="use_underline">True</property>
1975                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1976                                   <property name="focus_on_click">True</property>
1977                                 </widget>
1978                                 <packing>
1979                                   <property name="left_attach">1</property>
1980                                   <property name="right_attach">2</property>
1981                                   <property name="top_attach">14</property>
1982                                   <property name="bottom_attach">15</property>
1983                                   <property name="x_options">fill</property>
1984                                   <property name="y_options"></property>
1985                                 </packing>
1986                               </child>
1987
1988                               <child>
1989                                 <widget class="GtkButton" id="cutButton">
1990                                   <property name="visible">True</property>
1991                                   <property name="tooltip" translatable="yes">Cut</property>
1992                                   <property name="can_focus">True</property>
1993                                   <property name="label" translatable="yes">cut</property>
1994                                   <property name="use_underline">True</property>
1995                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1996                                   <property name="focus_on_click">True</property>
1997                                 </widget>
1998                                 <packing>
1999                                   <property name="left_attach">0</property>
2000                                   <property name="right_attach">1</property>
2001                                   <property name="top_attach">16</property>
2002                                   <property name="bottom_attach">17</property>
2003                                   <property name="x_options">fill</property>
2004                                   <property name="y_options"></property>
2005                                 </packing>
2006                               </child>
2007
2008                               <child>
2009                                 <widget class="GtkButton" id="replaceButton">
2010                                   <property name="visible">True</property>
2011                                   <property name="tooltip" translatable="yes">Replace</property>
2012                                   <property name="can_focus">True</property>
2013                                   <property name="label" translatable="yes">repl</property>
2014                                   <property name="use_underline">True</property>
2015                                   <property name="relief">GTK_RELIEF_NORMAL</property>
2016                                   <property name="focus_on_click">True</property>
2017                                 </widget>
2018                                 <packing>
2019                                   <property name="left_attach">1</property>
2020                                   <property name="right_attach">2</property>
2021                                   <property name="top_attach">16</property>
2022                                   <property name="bottom_attach">17</property>
2023                                   <property name="x_options">fill</property>
2024                                   <property name="y_options"></property>
2025                                 </packing>
2026                               </child>
2027
2028                               <child>
2029                                 <widget class="GtkButton" id="elimTypeButton">
2030                                   <property name="visible">True</property>
2031                                   <property name="tooltip" translatable="yes">ElimType</property>
2032                                   <property name="can_focus">True</property>
2033                                   <property name="label" translatable="yes">elimTy</property>
2034                                   <property name="use_underline">True</property>
2035                                   <property name="relief">GTK_RELIEF_NORMAL</property>
2036                                   <property name="focus_on_click">True</property>
2037                                 </widget>
2038                                 <packing>
2039                                   <property name="left_attach">1</property>
2040                                   <property name="right_attach">2</property>
2041                                   <property name="top_attach">4</property>
2042                                   <property name="bottom_attach">5</property>
2043                                   <property name="x_options">fill</property>
2044                                   <property name="y_options"></property>
2045                                 </packing>
2046                               </child>
2047
2048                               <child>
2049                                 <widget class="GtkHBox" id="hbox18">
2050                                   <property name="visible">True</property>
2051                                   <property name="homogeneous">True</property>
2052                                   <property name="spacing">0</property>
2053
2054                                   <child>
2055                                     <widget class="GtkButton" id="rightButton">
2056                                       <property name="visible">True</property>
2057                                       <property name="tooltip" translatable="yes">Right</property>
2058                                       <property name="can_focus">True</property>
2059                                       <property name="label" translatable="yes">R</property>
2060                                       <property name="use_underline">True</property>
2061                                       <property name="relief">GTK_RELIEF_NORMAL</property>
2062                                       <property name="focus_on_click">True</property>
2063                                     </widget>
2064                                     <packing>
2065                                       <property name="padding">0</property>
2066                                       <property name="expand">True</property>
2067                                       <property name="fill">True</property>
2068                                     </packing>
2069                                   </child>
2070
2071                                   <child>
2072                                     <widget class="GtkButton" id="existsButton">
2073                                       <property name="visible">True</property>
2074                                       <property name="tooltip" translatable="yes">Exists</property>
2075                                       <property name="can_focus">True</property>
2076                                       <property name="label" translatable="yes">∃</property>
2077                                       <property name="use_underline">True</property>
2078                                       <property name="relief">GTK_RELIEF_NORMAL</property>
2079                                       <property name="focus_on_click">True</property>
2080                                     </widget>
2081                                     <packing>
2082                                       <property name="padding">0</property>
2083                                       <property name="expand">True</property>
2084                                       <property name="fill">True</property>
2085                                     </packing>
2086                                   </child>
2087                                 </widget>
2088                                 <packing>
2089                                   <property name="left_attach">1</property>
2090                                   <property name="right_attach">2</property>
2091                                   <property name="top_attach">6</property>
2092                                   <property name="bottom_attach">7</property>
2093                                   <property name="x_options">fill</property>
2094                                   <property name="y_options">fill</property>
2095                                 </packing>
2096                               </child>
2097
2098                               <child>
2099                                 <widget class="GtkHBox" id="hbox17">
2100                                   <property name="visible">True</property>
2101                                   <property name="homogeneous">True</property>
2102                                   <property name="spacing">0</property>
2103
2104                                   <child>
2105                                     <widget class="GtkButton" id="splitButton">
2106                                       <property name="visible">True</property>
2107                                       <property name="tooltip" translatable="yes">Split</property>
2108                                       <property name="can_focus">True</property>
2109                                       <property name="label" translatable="yes">∧</property>
2110                                       <property name="use_underline">True</property>
2111                                       <property name="relief">GTK_RELIEF_NORMAL</property>
2112                                       <property name="focus_on_click">True</property>
2113                                     </widget>
2114                                     <packing>
2115                                       <property name="padding">0</property>
2116                                       <property name="expand">True</property>
2117                                       <property name="fill">True</property>
2118                                     </packing>
2119                                   </child>
2120
2121                                   <child>
2122                                     <widget class="GtkButton" id="leftButton">
2123                                       <property name="visible">True</property>
2124                                       <property name="tooltip" translatable="yes">Left</property>
2125                                       <property name="can_focus">True</property>
2126                                       <property name="label" translatable="yes">L</property>
2127                                       <property name="use_underline">True</property>
2128                                       <property name="relief">GTK_RELIEF_NORMAL</property>
2129                                       <property name="focus_on_click">True</property>
2130                                     </widget>
2131                                     <packing>
2132                                       <property name="padding">0</property>
2133                                       <property name="expand">True</property>
2134                                       <property name="fill">True</property>
2135                                     </packing>
2136                                   </child>
2137                                 </widget>
2138                                 <packing>
2139                                   <property name="left_attach">0</property>
2140                                   <property name="right_attach">1</property>
2141                                   <property name="top_attach">6</property>
2142                                   <property name="bottom_attach">7</property>
2143                                   <property name="x_options">fill</property>
2144                                   <property name="y_options">fill</property>
2145                                 </packing>
2146                               </child>
2147
2148                               <child>
2149                                 <widget class="GtkAlignment" id="alignment6">
2150                                   <property name="visible">True</property>
2151                                   <property name="xalign">0.5</property>
2152                                   <property name="yalign">0.5</property>
2153                                   <property name="xscale">1</property>
2154                                   <property name="yscale">1</property>
2155                                   <property name="top_padding">0</property>
2156                                   <property name="bottom_padding">0</property>
2157                                   <property name="left_padding">0</property>
2158                                   <property name="right_padding">0</property>
2159
2160                                   <child>
2161                                     <placeholder/>
2162                                   </child>
2163                                 </widget>
2164                                 <packing>
2165                                   <property name="left_attach">0</property>
2166                                   <property name="right_attach">1</property>
2167                                   <property name="top_attach">1</property>
2168                                   <property name="bottom_attach">2</property>
2169                                   <property name="x_options">fill</property>
2170                                 </packing>
2171                               </child>
2172
2173                               <child>
2174                                 <widget class="GtkAlignment" id="alignment7">
2175                                   <property name="visible">True</property>
2176                                   <property name="xalign">0.5</property>
2177                                   <property name="yalign">0.5</property>
2178                                   <property name="xscale">1</property>
2179                                   <property name="yscale">1</property>
2180                                   <property name="top_padding">0</property>
2181                                   <property name="bottom_padding">0</property>
2182                                   <property name="left_padding">0</property>
2183                                   <property name="right_padding">0</property>
2184
2185                                   <child>
2186                                     <placeholder/>
2187                                   </child>
2188                                 </widget>
2189                                 <packing>
2190                                   <property name="left_attach">0</property>
2191                                   <property name="right_attach">1</property>
2192                                   <property name="top_attach">3</property>
2193                                   <property name="bottom_attach">4</property>
2194                                   <property name="x_options">fill</property>
2195                                 </packing>
2196                               </child>
2197
2198                               <child>
2199                                 <widget class="GtkAlignment" id="alignment8">
2200                                   <property name="visible">True</property>
2201                                   <property name="xalign">0.5</property>
2202                                   <property name="yalign">0.5</property>
2203                                   <property name="xscale">1</property>
2204                                   <property name="yscale">1</property>
2205                                   <property name="top_padding">0</property>
2206                                   <property name="bottom_padding">0</property>
2207                                   <property name="left_padding">0</property>
2208                                   <property name="right_padding">0</property>
2209
2210                                   <child>
2211                                     <placeholder/>
2212                                   </child>
2213                                 </widget>
2214                                 <packing>
2215                                   <property name="left_attach">0</property>
2216                                   <property name="right_attach">1</property>
2217                                   <property name="top_attach">5</property>
2218                                   <property name="bottom_attach">6</property>
2219                                   <property name="x_options">fill</property>
2220                                 </packing>
2221                               </child>
2222
2223                               <child>
2224                                 <widget class="GtkAlignment" id="alignment9">
2225                                   <property name="visible">True</property>
2226                                   <property name="xalign">0.5</property>
2227                                   <property name="yalign">0.5</property>
2228                                   <property name="xscale">1</property>
2229                                   <property name="yscale">1</property>
2230                                   <property name="top_padding">0</property>
2231                                   <property name="bottom_padding">0</property>
2232                                   <property name="left_padding">0</property>
2233                                   <property name="right_padding">0</property>
2234
2235                                   <child>
2236                                     <placeholder/>
2237                                   </child>
2238                                 </widget>
2239                                 <packing>
2240                                   <property name="left_attach">0</property>
2241                                   <property name="right_attach">1</property>
2242                                   <property name="top_attach">7</property>
2243                                   <property name="bottom_attach">8</property>
2244                                   <property name="x_options">fill</property>
2245                                 </packing>
2246                               </child>
2247
2248                               <child>
2249                                 <widget class="GtkAlignment" id="alignment10">
2250                                   <property name="visible">True</property>
2251                                   <property name="xalign">0.5</property>
2252                                   <property name="yalign">0.5</property>
2253                                   <property name="xscale">1</property>
2254                                   <property name="yscale">1</property>
2255                                   <property name="top_padding">0</property>
2256                                   <property name="bottom_padding">0</property>
2257                                   <property name="left_padding">0</property>
2258                                   <property name="right_padding">0</property>
2259
2260                                   <child>
2261                                     <placeholder/>
2262                                   </child>
2263                                 </widget>
2264                                 <packing>
2265                                   <property name="left_attach">0</property>
2266                                   <property name="right_attach">1</property>
2267                                   <property name="top_attach">10</property>
2268                                   <property name="bottom_attach">11</property>
2269                                   <property name="x_options">fill</property>
2270                                 </packing>
2271                               </child>
2272
2273                               <child>
2274                                 <widget class="GtkAlignment" id="alignment11">
2275                                   <property name="visible">True</property>
2276                                   <property name="xalign">0.5</property>
2277                                   <property name="yalign">0.5</property>
2278                                   <property name="xscale">1</property>
2279                                   <property name="yscale">1</property>
2280                                   <property name="top_padding">0</property>
2281                                   <property name="bottom_padding">0</property>
2282                                   <property name="left_padding">0</property>
2283                                   <property name="right_padding">0</property>
2284
2285                                   <child>
2286                                     <placeholder/>
2287                                   </child>
2288                                 </widget>
2289                                 <packing>
2290                                   <property name="left_attach">0</property>
2291                                   <property name="right_attach">1</property>
2292                                   <property name="top_attach">13</property>
2293                                   <property name="bottom_attach">14</property>
2294                                   <property name="x_options">fill</property>
2295                                 </packing>
2296                               </child>
2297
2298                               <child>
2299                                 <widget class="GtkAlignment" id="alignment12">
2300                                   <property name="visible">True</property>
2301                                   <property name="xalign">0.5</property>
2302                                   <property name="yalign">0.5</property>
2303                                   <property name="xscale">1</property>
2304                                   <property name="yscale">1</property>
2305                                   <property name="top_padding">0</property>
2306                                   <property name="bottom_padding">0</property>
2307                                   <property name="left_padding">0</property>
2308                                   <property name="right_padding">0</property>
2309
2310                                   <child>
2311                                     <placeholder/>
2312                                   </child>
2313                                 </widget>
2314                                 <packing>
2315                                   <property name="left_attach">0</property>
2316                                   <property name="right_attach">1</property>
2317                                   <property name="top_attach">15</property>
2318                                   <property name="bottom_attach">16</property>
2319                                   <property name="x_options">fill</property>
2320                                 </packing>
2321                               </child>
2322                             </widget>
2323                           </child>
2324                         </widget>
2325                         <packing>
2326                           <property name="padding">0</property>
2327                           <property name="expand">False</property>
2328                           <property name="fill">True</property>
2329                         </packing>
2330                       </child>
2331
2332                       <child>
2333                         <widget class="GtkVBox" id="vboxScript">
2334                           <property name="width_request">400</property>
2335                           <property name="visible">True</property>
2336                           <property name="homogeneous">False</property>
2337                           <property name="spacing">0</property>
2338
2339                           <child>
2340                             <widget class="GtkHBox" id="hbox28">
2341                               <property name="visible">True</property>
2342                               <property name="homogeneous">False</property>
2343                               <property name="spacing">0</property>
2344
2345                               <child>
2346                                 <widget class="GtkToolbar" id="buttonsToolbar">
2347                                   <property name="visible">True</property>
2348                                   <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
2349                                   <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
2350                                   <property name="tooltips">True</property>
2351                                   <property name="show_arrow">True</property>
2352
2353                                   <child>
2354                                     <widget class="GtkToolItem" id="toolitem41">
2355                                       <property name="visible">True</property>
2356                                       <property name="visible_horizontal">True</property>
2357                                       <property name="visible_vertical">True</property>
2358                                       <property name="is_important">False</property>
2359
2360                                       <child>
2361                                         <widget class="GtkButton" id="scriptTopButton">
2362                                           <property name="visible">True</property>
2363                                           <property name="tooltip" translatable="yes">Restart</property>
2364                                           <property name="can_focus">True</property>
2365                                           <property name="relief">GTK_RELIEF_NONE</property>
2366                                           <property name="focus_on_click">True</property>
2367
2368                                           <child>
2369                                             <widget class="GtkImage" id="image920">
2370                                               <property name="visible">True</property>
2371                                               <property name="stock">gtk-goto-top</property>
2372                                               <property name="icon_size">4</property>
2373                                               <property name="xalign">0.5</property>
2374                                               <property name="yalign">0.5</property>
2375                                               <property name="xpad">0</property>
2376                                               <property name="ypad">0</property>
2377                                             </widget>
2378                                           </child>
2379                                         </widget>
2380                                       </child>
2381                                     </widget>
2382                                     <packing>
2383                                       <property name="expand">False</property>
2384                                       <property name="homogeneous">False</property>
2385                                     </packing>
2386                                   </child>
2387
2388                                   <child>
2389                                     <widget class="GtkToolItem" id="toolitem42">
2390                                       <property name="visible">True</property>
2391                                       <property name="visible_horizontal">True</property>
2392                                       <property name="visible_vertical">True</property>
2393                                       <property name="is_important">False</property>
2394
2395                                       <child>
2396                                         <widget class="GtkButton" id="scriptRetractButton">
2397                                           <property name="visible">True</property>
2398                                           <property name="tooltip" translatable="yes">Retract 1 phrase</property>
2399                                           <property name="can_focus">True</property>
2400                                           <property name="relief">GTK_RELIEF_NONE</property>
2401                                           <property name="focus_on_click">True</property>
2402
2403                                           <child>
2404                                             <widget class="GtkImage" id="image921">
2405                                               <property name="visible">True</property>
2406                                               <property name="stock">gtk-go-up</property>
2407                                               <property name="icon_size">4</property>
2408                                               <property name="xalign">0.5</property>
2409                                               <property name="yalign">0.5</property>
2410                                               <property name="xpad">0</property>
2411                                               <property name="ypad">0</property>
2412                                             </widget>
2413                                           </child>
2414                                         </widget>
2415                                       </child>
2416                                     </widget>
2417                                     <packing>
2418                                       <property name="expand">False</property>
2419                                       <property name="homogeneous">False</property>
2420                                     </packing>
2421                                   </child>
2422
2423                                   <child>
2424                                     <widget class="GtkToolItem" id="toolitem43">
2425                                       <property name="visible">True</property>
2426                                       <property name="visible_horizontal">True</property>
2427                                       <property name="visible_vertical">True</property>
2428                                       <property name="is_important">False</property>
2429
2430                                       <child>
2431                                         <widget class="GtkButton" id="scriptJumpButton">
2432                                           <property name="visible">True</property>
2433                                           <property name="tooltip" translatable="yes">Execute until point</property>
2434                                           <property name="can_focus">True</property>
2435                                           <property name="relief">GTK_RELIEF_NONE</property>
2436                                           <property name="focus_on_click">True</property>
2437
2438                                           <child>
2439                                             <widget class="GtkImage" id="image922">
2440                                               <property name="visible">True</property>
2441                                               <property name="stock">gtk-jump-to</property>
2442                                               <property name="icon_size">4</property>
2443                                               <property name="xalign">0.5</property>
2444                                               <property name="yalign">0.5</property>
2445                                               <property name="xpad">0</property>
2446                                               <property name="ypad">0</property>
2447                                             </widget>
2448                                           </child>
2449                                         </widget>
2450                                       </child>
2451                                     </widget>
2452                                     <packing>
2453                                       <property name="expand">False</property>
2454                                       <property name="homogeneous">False</property>
2455                                     </packing>
2456                                   </child>
2457
2458                                   <child>
2459                                     <widget class="GtkToolItem" id="toolitem44">
2460                                       <property name="visible">True</property>
2461                                       <property name="visible_horizontal">True</property>
2462                                       <property name="visible_vertical">True</property>
2463                                       <property name="is_important">False</property>
2464
2465                                       <child>
2466                                         <widget class="GtkButton" id="scriptAdvanceButton">
2467                                           <property name="visible">True</property>
2468                                           <property name="tooltip" translatable="yes">Execute 1 phrase</property>
2469                                           <property name="can_focus">True</property>
2470                                           <property name="relief">GTK_RELIEF_NONE</property>
2471                                           <property name="focus_on_click">True</property>
2472
2473                                           <child>
2474                                             <widget class="GtkImage" id="image923">
2475                                               <property name="visible">True</property>
2476                                               <property name="stock">gtk-go-down</property>
2477                                               <property name="icon_size">4</property>
2478                                               <property name="xalign">0.5</property>
2479                                               <property name="yalign">0.5</property>
2480                                               <property name="xpad">0</property>
2481                                               <property name="ypad">0</property>
2482                                             </widget>
2483                                           </child>
2484                                         </widget>
2485                                       </child>
2486                                     </widget>
2487                                     <packing>
2488                                       <property name="expand">False</property>
2489                                       <property name="homogeneous">False</property>
2490                                     </packing>
2491                                   </child>
2492
2493                                   <child>
2494                                     <widget class="GtkToolItem" id="toolitem45">
2495                                       <property name="visible">True</property>
2496                                       <property name="visible_horizontal">True</property>
2497                                       <property name="visible_vertical">True</property>
2498                                       <property name="is_important">False</property>
2499
2500                                       <child>
2501                                         <widget class="GtkButton" id="scriptBottomButton">
2502                                           <property name="visible">True</property>
2503                                           <property name="tooltip" translatable="yes">Execute all</property>
2504                                           <property name="can_focus">True</property>
2505                                           <property name="relief">GTK_RELIEF_NONE</property>
2506                                           <property name="focus_on_click">True</property>
2507
2508                                           <child>
2509                                             <widget class="GtkImage" id="image924">
2510                                               <property name="visible">True</property>
2511                                               <property name="stock">gtk-goto-bottom</property>
2512                                               <property name="icon_size">4</property>
2513                                               <property name="xalign">0.5</property>
2514                                               <property name="yalign">0.5</property>
2515                                               <property name="xpad">0</property>
2516                                               <property name="ypad">0</property>
2517                                             </widget>
2518                                           </child>
2519                                         </widget>
2520                                       </child>
2521                                     </widget>
2522                                     <packing>
2523                                       <property name="expand">False</property>
2524                                       <property name="homogeneous">False</property>
2525                                     </packing>
2526                                   </child>
2527                                 </widget>
2528                                 <packing>
2529                                   <property name="padding">0</property>
2530                                   <property name="expand">True</property>
2531                                   <property name="fill">True</property>
2532                                 </packing>
2533                               </child>
2534
2535                               <child>
2536                                 <widget class="GtkToolbar" id="toolbar2">
2537                                   <property name="visible">True</property>
2538                                   <property name="orientation">GTK_ORIENTATION_VERTICAL</property>
2539                                   <property name="toolbar_style">GTK_TOOLBAR_ICONS</property>
2540                                   <property name="tooltips">True</property>
2541                                   <property name="show_arrow">True</property>
2542
2543                                   <child>
2544                                     <widget class="GtkToolItem" id="toolitem46">
2545                                       <property name="visible">True</property>
2546                                       <property name="visible_horizontal">True</property>
2547                                       <property name="visible_vertical">True</property>
2548                                       <property name="is_important">False</property>
2549
2550                                       <child>
2551                                         <widget class="GtkButton" id="scriptAbortButton">
2552                                           <property name="visible">True</property>
2553                                           <property name="can_focus">True</property>
2554                                           <property name="relief">GTK_RELIEF_NONE</property>
2555                                           <property name="focus_on_click">True</property>
2556
2557                                           <child>
2558                                             <widget class="GtkImage" id="image927">
2559                                               <property name="visible">True</property>
2560                                               <property name="stock">gtk-stop</property>
2561                                               <property name="icon_size">4</property>
2562                                               <property name="xalign">0.5</property>
2563                                               <property name="yalign">0.5</property>
2564                                               <property name="xpad">0</property>
2565                                               <property name="ypad">0</property>
2566                                             </widget>
2567                                           </child>
2568                                         </widget>
2569                                       </child>
2570                                     </widget>
2571                                     <packing>
2572                                       <property name="expand">False</property>
2573                                       <property name="homogeneous">False</property>
2574                                     </packing>
2575                                   </child>
2576                                 </widget>
2577                                 <packing>
2578                                   <property name="padding">0</property>
2579                                   <property name="expand">False</property>
2580                                   <property name="fill">True</property>
2581                                 </packing>
2582                               </child>
2583                             </widget>
2584                             <packing>
2585                               <property name="padding">0</property>
2586                               <property name="expand">False</property>
2587                               <property name="fill">False</property>
2588                             </packing>
2589                           </child>
2590
2591                           <child>
2592                             <widget class="GtkNotebook" id="scriptNotebook">
2593                               <property name="visible">True</property>
2594                               <property name="can_focus">True</property>
2595                               <property name="show_tabs">True</property>
2596                               <property name="show_border">True</property>
2597                               <property name="tab_pos">GTK_POS_BOTTOM</property>
2598                               <property name="scrollable">False</property>
2599                               <property name="enable_popup">False</property>
2600
2601                               <child>
2602                                 <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
2603                                   <property name="visible">True</property>
2604                                   <property name="can_focus">True</property>
2605                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2606                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2607                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2608                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2609
2610                                   <child>
2611                                     <placeholder/>
2612                                   </child>
2613                                 </widget>
2614                                 <packing>
2615                                   <property name="tab_expand">False</property>
2616                                   <property name="tab_fill">True</property>
2617                                 </packing>
2618                               </child>
2619
2620                               <child>
2621                                 <widget class="GtkLabel" id="scriptLabel">
2622                                   <property name="visible">True</property>
2623                                   <property name="label" translatable="yes">script</property>
2624                                   <property name="use_underline">False</property>
2625                                   <property name="use_markup">False</property>
2626                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2627                                   <property name="wrap">False</property>
2628                                   <property name="selectable">False</property>
2629                                   <property name="xalign">0.5</property>
2630                                   <property name="yalign">0.5</property>
2631                                   <property name="xpad">0</property>
2632                                   <property name="ypad">0</property>
2633                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2634                                   <property name="width_chars">-1</property>
2635                                   <property name="single_line_mode">False</property>
2636                                   <property name="angle">0</property>
2637                                 </widget>
2638                                 <packing>
2639                                   <property name="type">tab</property>
2640                                 </packing>
2641                               </child>
2642
2643                               <child>
2644                                 <widget class="GtkScrolledWindow" id="scrolledwindow8">
2645                                   <property name="visible">True</property>
2646                                   <property name="can_focus">True</property>
2647                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2648                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2649                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2650                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2651
2652                                   <child>
2653                                     <widget class="GtkViewport" id="viewport1">
2654                                       <property name="visible">True</property>
2655                                       <property name="shadow_type">GTK_SHADOW_IN</property>
2656
2657                                       <child>
2658                                         <widget class="GtkLabel" id="label25">
2659                                           <property name="visible">True</property>
2660                                           <property name="label" translatable="yes">Not implemented.</property>
2661                                           <property name="use_underline">False</property>
2662                                           <property name="use_markup">False</property>
2663                                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2664                                           <property name="wrap">False</property>
2665                                           <property name="selectable">False</property>
2666                                           <property name="xalign">0.5</property>
2667                                           <property name="yalign">0.5</property>
2668                                           <property name="xpad">0</property>
2669                                           <property name="ypad">0</property>
2670                                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2671                                           <property name="width_chars">-1</property>
2672                                           <property name="single_line_mode">False</property>
2673                                           <property name="angle">0</property>
2674                                         </widget>
2675                                       </child>
2676                                     </widget>
2677                                   </child>
2678                                 </widget>
2679                                 <packing>
2680                                   <property name="tab_expand">False</property>
2681                                   <property name="tab_fill">True</property>
2682                                 </packing>
2683                               </child>
2684
2685                               <child>
2686                                 <widget class="GtkLabel" id="label13">
2687                                   <property name="visible">True</property>
2688                                   <property name="label" translatable="yes">outline</property>
2689                                   <property name="use_underline">False</property>
2690                                   <property name="use_markup">False</property>
2691                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2692                                   <property name="wrap">False</property>
2693                                   <property name="selectable">False</property>
2694                                   <property name="xalign">0.5</property>
2695                                   <property name="yalign">0.5</property>
2696                                   <property name="xpad">0</property>
2697                                   <property name="ypad">0</property>
2698                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2699                                   <property name="width_chars">-1</property>
2700                                   <property name="single_line_mode">False</property>
2701                                   <property name="angle">0</property>
2702                                 </widget>
2703                                 <packing>
2704                                   <property name="type">tab</property>
2705                                 </packing>
2706                               </child>
2707                             </widget>
2708                             <packing>
2709                               <property name="padding">0</property>
2710                               <property name="expand">True</property>
2711                               <property name="fill">True</property>
2712                             </packing>
2713                           </child>
2714                         </widget>
2715                         <packing>
2716                           <property name="padding">0</property>
2717                           <property name="expand">True</property>
2718                           <property name="fill">True</property>
2719                         </packing>
2720                       </child>
2721                     </widget>
2722                     <packing>
2723                       <property name="shrink">True</property>
2724                       <property name="resize">False</property>
2725                     </packing>
2726                   </child>
2727
2728                   <child>
2729                     <widget class="GtkVPaned" id="vpaned1">
2730                       <property name="width_request">250</property>
2731                       <property name="height_request">500</property>
2732                       <property name="visible">True</property>
2733                       <property name="can_focus">True</property>
2734                       <property name="position">380</property>
2735
2736                       <child>
2737                         <widget class="GtkNotebook" id="sequentsNotebook">
2738                           <property name="visible">True</property>
2739                           <property name="can_focus">True</property>
2740                           <property name="show_tabs">True</property>
2741                           <property name="show_border">True</property>
2742                           <property name="tab_pos">GTK_POS_TOP</property>
2743                           <property name="scrollable">False</property>
2744                           <property name="enable_popup">False</property>
2745                         </widget>
2746                         <packing>
2747                           <property name="shrink">True</property>
2748                           <property name="resize">False</property>
2749                         </packing>
2750                       </child>
2751
2752                       <child>
2753                         <widget class="GtkHBox" id="hbox9">
2754                           <property name="visible">True</property>
2755                           <property name="homogeneous">False</property>
2756                           <property name="spacing">0</property>
2757
2758                           <child>
2759                             <widget class="GtkScrolledWindow" id="logScrolledWin">
2760                               <property name="visible">True</property>
2761                               <property name="can_focus">True</property>
2762                               <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
2763                               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2764                               <property name="shadow_type">GTK_SHADOW_IN</property>
2765                               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2766
2767                               <child>
2768                                 <widget class="GtkTextView" id="logTextView">
2769                                   <property name="visible">True</property>
2770                                   <property name="can_focus">True</property>
2771                                   <property name="editable">False</property>
2772                                   <property name="overwrite">False</property>
2773                                   <property name="accepts_tab">True</property>
2774                                   <property name="justification">GTK_JUSTIFY_LEFT</property>
2775                                   <property name="wrap_mode">GTK_WRAP_CHAR</property>
2776                                   <property name="cursor_visible">False</property>
2777                                   <property name="pixels_above_lines">0</property>
2778                                   <property name="pixels_below_lines">0</property>
2779                                   <property name="pixels_inside_wrap">0</property>
2780                                   <property name="left_margin">0</property>
2781                                   <property name="right_margin">0</property>
2782                                   <property name="indent">0</property>
2783                                   <property name="text" translatable="yes"></property>
2784                                 </widget>
2785                               </child>
2786                             </widget>
2787                             <packing>
2788                               <property name="padding">0</property>
2789                               <property name="expand">True</property>
2790                               <property name="fill">True</property>
2791                             </packing>
2792                           </child>
2793                         </widget>
2794                         <packing>
2795                           <property name="shrink">True</property>
2796                           <property name="resize">True</property>
2797                         </packing>
2798                       </child>
2799                     </widget>
2800                     <packing>
2801                       <property name="shrink">True</property>
2802                       <property name="resize">True</property>
2803                     </packing>
2804                   </child>
2805                 </widget>
2806                 <packing>
2807                   <property name="padding">0</property>
2808                   <property name="expand">True</property>
2809                   <property name="fill">True</property>
2810                 </packing>
2811               </child>
2812             </widget>
2813             <packing>
2814               <property name="padding">0</property>
2815               <property name="expand">True</property>
2816               <property name="fill">True</property>
2817             </packing>
2818           </child>
2819
2820           <child>
2821             <widget class="GtkHBox" id="hbox10">
2822               <property name="visible">True</property>
2823               <property name="homogeneous">False</property>
2824               <property name="spacing">0</property>
2825
2826               <child>
2827                 <widget class="GtkStatusbar" id="StatusBar">
2828                   <property name="visible">True</property>
2829                   <property name="has_resize_grip">False</property>
2830                 </widget>
2831                 <packing>
2832                   <property name="padding">0</property>
2833                   <property name="expand">True</property>
2834                   <property name="fill">True</property>
2835                 </packing>
2836               </child>
2837
2838               <child>
2839                 <widget class="GtkNotebook" id="HintNotebook">
2840                   <property name="visible">True</property>
2841                   <property name="show_tabs">False</property>
2842                   <property name="show_border">True</property>
2843                   <property name="tab_pos">GTK_POS_TOP</property>
2844                   <property name="scrollable">False</property>
2845                   <property name="enable_popup">False</property>
2846
2847                   <child>
2848                     <widget class="GtkImage" id="HintLowImage">
2849                       <property name="visible">True</property>
2850                       <property name="xalign">0.5</property>
2851                       <property name="yalign">0.5</property>
2852                       <property name="xpad">0</property>
2853                       <property name="ypad">0</property>
2854                     </widget>
2855                     <packing>
2856                       <property name="tab_expand">False</property>
2857                       <property name="tab_fill">True</property>
2858                     </packing>
2859                   </child>
2860
2861                   <child>
2862                     <widget class="GtkLabel" id="label14">
2863                       <property name="visible">True</property>
2864                       <property name="label" translatable="yes">label14</property>
2865                       <property name="use_underline">False</property>
2866                       <property name="use_markup">False</property>
2867                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2868                       <property name="wrap">False</property>
2869                       <property name="selectable">False</property>
2870                       <property name="xalign">0.5</property>
2871                       <property name="yalign">0.5</property>
2872                       <property name="xpad">0</property>
2873                       <property name="ypad">0</property>
2874                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2875                       <property name="width_chars">-1</property>
2876                       <property name="single_line_mode">False</property>
2877                       <property name="angle">0</property>
2878                     </widget>
2879                     <packing>
2880                       <property name="type">tab</property>
2881                     </packing>
2882                   </child>
2883
2884                   <child>
2885                     <widget class="GtkImage" id="HintMediumImage">
2886                       <property name="visible">True</property>
2887                       <property name="xalign">0.5</property>
2888                       <property name="yalign">0.5</property>
2889                       <property name="xpad">0</property>
2890                       <property name="ypad">0</property>
2891                     </widget>
2892                     <packing>
2893                       <property name="tab_expand">False</property>
2894                       <property name="tab_fill">True</property>
2895                     </packing>
2896                   </child>
2897
2898                   <child>
2899                     <widget class="GtkLabel" id="label15">
2900                       <property name="visible">True</property>
2901                       <property name="label" translatable="yes">label15</property>
2902                       <property name="use_underline">False</property>
2903                       <property name="use_markup">False</property>
2904                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2905                       <property name="wrap">False</property>
2906                       <property name="selectable">False</property>
2907                       <property name="xalign">0.5</property>
2908                       <property name="yalign">0.5</property>
2909                       <property name="xpad">0</property>
2910                       <property name="ypad">0</property>
2911                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2912                       <property name="width_chars">-1</property>
2913                       <property name="single_line_mode">False</property>
2914                       <property name="angle">0</property>
2915                     </widget>
2916                     <packing>
2917                       <property name="type">tab</property>
2918                     </packing>
2919                   </child>
2920
2921                   <child>
2922                     <widget class="GtkImage" id="HintHighImage">
2923                       <property name="visible">True</property>
2924                       <property name="xalign">0.5</property>
2925                       <property name="yalign">0.5</property>
2926                       <property name="xpad">0</property>
2927                       <property name="ypad">0</property>
2928                     </widget>
2929                     <packing>
2930                       <property name="tab_expand">False</property>
2931                       <property name="tab_fill">True</property>
2932                     </packing>
2933                   </child>
2934
2935                   <child>
2936                     <widget class="GtkLabel" id="label16">
2937                       <property name="visible">True</property>
2938                       <property name="label" translatable="yes">label16</property>
2939                       <property name="use_underline">False</property>
2940                       <property name="use_markup">False</property>
2941                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2942                       <property name="wrap">False</property>
2943                       <property name="selectable">False</property>
2944                       <property name="xalign">0.5</property>
2945                       <property name="yalign">0.5</property>
2946                       <property name="xpad">0</property>
2947                       <property name="ypad">0</property>
2948                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2949                       <property name="width_chars">-1</property>
2950                       <property name="single_line_mode">False</property>
2951                       <property name="angle">0</property>
2952                     </widget>
2953                     <packing>
2954                       <property name="type">tab</property>
2955                     </packing>
2956                   </child>
2957                 </widget>
2958                 <packing>
2959                   <property name="padding">0</property>
2960                   <property name="expand">False</property>
2961                   <property name="fill">True</property>
2962                 </packing>
2963               </child>
2964             </widget>
2965             <packing>
2966               <property name="padding">0</property>
2967               <property name="expand">False</property>
2968               <property name="fill">False</property>
2969             </packing>
2970           </child>
2971         </widget>
2972       </child>
2973     </widget>
2974   </child>
2975 </widget>
2976
2977 <widget class="GtkDialog" id="TextDialog">
2978   <property name="title" translatable="yes">DUMMY</property>
2979   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2980   <property name="window_position">GTK_WIN_POS_NONE</property>
2981   <property name="modal">False</property>
2982   <property name="resizable">True</property>
2983   <property name="destroy_with_parent">False</property>
2984   <property name="decorated">True</property>
2985   <property name="skip_taskbar_hint">False</property>
2986   <property name="skip_pager_hint">False</property>
2987   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2988   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2989   <property name="focus_on_map">True</property>
2990   <property name="urgency_hint">False</property>
2991   <property name="has_separator">True</property>
2992
2993   <child internal-child="vbox">
2994     <widget class="GtkVBox" id="vbox5">
2995       <property name="visible">True</property>
2996       <property name="homogeneous">False</property>
2997       <property name="spacing">0</property>
2998
2999       <child internal-child="action_area">
3000         <widget class="GtkHButtonBox" id="hbuttonbox1">
3001           <property name="visible">True</property>
3002           <property name="layout_style">GTK_BUTTONBOX_END</property>
3003
3004           <child>
3005             <widget class="GtkButton" id="TextDialogCancelButton">
3006               <property name="visible">True</property>
3007               <property name="can_default">True</property>
3008               <property name="can_focus">True</property>
3009               <property name="label">gtk-cancel</property>
3010               <property name="use_stock">True</property>
3011               <property name="relief">GTK_RELIEF_NORMAL</property>
3012               <property name="focus_on_click">True</property>
3013               <property name="response_id">-6</property>
3014             </widget>
3015           </child>
3016
3017           <child>
3018             <widget class="GtkButton" id="TextDialogOkButton">
3019               <property name="visible">True</property>
3020               <property name="can_default">True</property>
3021               <property name="can_focus">True</property>
3022               <property name="label">gtk-ok</property>
3023               <property name="use_stock">True</property>
3024               <property name="relief">GTK_RELIEF_NORMAL</property>
3025               <property name="focus_on_click">True</property>
3026               <property name="response_id">-5</property>
3027             </widget>
3028           </child>
3029         </widget>
3030         <packing>
3031           <property name="padding">0</property>
3032           <property name="expand">False</property>
3033           <property name="fill">True</property>
3034           <property name="pack_type">GTK_PACK_END</property>
3035         </packing>
3036       </child>
3037
3038       <child>
3039         <widget class="GtkLabel" id="TextDialogLabel">
3040           <property name="visible">True</property>
3041           <property name="label" translatable="yes">DUMMY</property>
3042           <property name="use_underline">False</property>
3043           <property name="use_markup">False</property>
3044           <property name="justify">GTK_JUSTIFY_LEFT</property>
3045           <property name="wrap">False</property>
3046           <property name="selectable">False</property>
3047           <property name="xalign">0.5</property>
3048           <property name="yalign">0.5</property>
3049           <property name="xpad">0</property>
3050           <property name="ypad">0</property>
3051           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3052           <property name="width_chars">-1</property>
3053           <property name="single_line_mode">False</property>
3054           <property name="angle">0</property>
3055         </widget>
3056         <packing>
3057           <property name="padding">0</property>
3058           <property name="expand">False</property>
3059           <property name="fill">False</property>
3060         </packing>
3061       </child>
3062
3063       <child>
3064         <widget class="GtkScrolledWindow" id="scrolledwindow2">
3065           <property name="visible">True</property>
3066           <property name="can_focus">True</property>
3067           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3068           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3069           <property name="shadow_type">GTK_SHADOW_IN</property>
3070           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3071
3072           <child>
3073             <widget class="GtkTextView" id="TextDialogTextView">
3074               <property name="visible">True</property>
3075               <property name="can_focus">True</property>
3076               <property name="editable">True</property>
3077               <property name="overwrite">False</property>
3078               <property name="accepts_tab">True</property>
3079               <property name="justification">GTK_JUSTIFY_LEFT</property>
3080               <property name="wrap_mode">GTK_WRAP_NONE</property>
3081               <property name="cursor_visible">True</property>
3082               <property name="pixels_above_lines">0</property>
3083               <property name="pixels_below_lines">0</property>
3084               <property name="pixels_inside_wrap">0</property>
3085               <property name="left_margin">0</property>
3086               <property name="right_margin">0</property>
3087               <property name="indent">0</property>
3088               <property name="text" translatable="yes"></property>
3089             </widget>
3090           </child>
3091         </widget>
3092         <packing>
3093           <property name="padding">0</property>
3094           <property name="expand">True</property>
3095           <property name="fill">True</property>
3096         </packing>
3097       </child>
3098     </widget>
3099   </child>
3100 </widget>
3101
3102 <widget class="GtkDialog" id="UriChoiceDialog">
3103   <property name="height_request">280</property>
3104   <property name="title" translatable="yes">Uri choice</property>
3105   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3106   <property name="window_position">GTK_WIN_POS_CENTER</property>
3107   <property name="modal">True</property>
3108   <property name="resizable">True</property>
3109   <property name="destroy_with_parent">False</property>
3110   <property name="decorated">True</property>
3111   <property name="skip_taskbar_hint">False</property>
3112   <property name="skip_pager_hint">False</property>
3113   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3114   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3115   <property name="focus_on_map">True</property>
3116   <property name="urgency_hint">False</property>
3117   <property name="has_separator">True</property>
3118
3119   <child internal-child="vbox">
3120     <widget class="GtkVBox" id="dialog-vbox3">
3121       <property name="visible">True</property>
3122       <property name="homogeneous">False</property>
3123       <property name="spacing">4</property>
3124
3125       <child internal-child="action_area">
3126         <widget class="GtkHButtonBox" id="dialog-action_area3">
3127           <property name="visible">True</property>
3128           <property name="layout_style">GTK_BUTTONBOX_END</property>
3129
3130           <child>
3131             <widget class="GtkButton" id="UriChoiceAbortButton">
3132               <property name="visible">True</property>
3133               <property name="can_default">True</property>
3134               <property name="can_focus">True</property>
3135               <property name="label">gtk-cancel</property>
3136               <property name="use_stock">True</property>
3137               <property name="relief">GTK_RELIEF_NORMAL</property>
3138               <property name="focus_on_click">True</property>
3139               <property name="response_id">-6</property>
3140             </widget>
3141           </child>
3142
3143           <child>
3144             <widget class="GtkButton" id="UriChoiceSelectedButton">
3145               <property name="visible">True</property>
3146               <property name="can_default">True</property>
3147               <property name="can_focus">True</property>
3148               <property name="relief">GTK_RELIEF_NORMAL</property>
3149               <property name="focus_on_click">True</property>
3150               <property name="response_id">0</property>
3151
3152               <child>
3153                 <widget class="GtkAlignment" id="alignment2">
3154                   <property name="visible">True</property>
3155                   <property name="xalign">0.5</property>
3156                   <property name="yalign">0.5</property>
3157                   <property name="xscale">0</property>
3158                   <property name="yscale">0</property>
3159                   <property name="top_padding">0</property>
3160                   <property name="bottom_padding">0</property>
3161                   <property name="left_padding">0</property>
3162                   <property name="right_padding">0</property>
3163
3164                   <child>
3165                     <widget class="GtkHBox" id="hbox3">
3166                       <property name="visible">True</property>
3167                       <property name="homogeneous">False</property>
3168                       <property name="spacing">2</property>
3169
3170                       <child>
3171                         <widget class="GtkImage" id="image19">
3172                           <property name="visible">True</property>
3173                           <property name="stock">gtk-index</property>
3174                           <property name="icon_size">4</property>
3175                           <property name="xalign">0.5</property>
3176                           <property name="yalign">0.5</property>
3177                           <property name="xpad">0</property>
3178                           <property name="ypad">0</property>
3179                         </widget>
3180                         <packing>
3181                           <property name="padding">0</property>
3182                           <property name="expand">False</property>
3183                           <property name="fill">False</property>
3184                         </packing>
3185                       </child>
3186
3187                       <child>
3188                         <widget class="GtkLabel" id="label3">
3189                           <property name="visible">True</property>
3190                           <property name="label" translatable="yes">Try _Selected</property>
3191                           <property name="use_underline">True</property>
3192                           <property name="use_markup">False</property>
3193                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3194                           <property name="wrap">False</property>
3195                           <property name="selectable">False</property>
3196                           <property name="xalign">0.5</property>
3197                           <property name="yalign">0.5</property>
3198                           <property name="xpad">0</property>
3199                           <property name="ypad">0</property>
3200                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3201                           <property name="width_chars">-1</property>
3202                           <property name="single_line_mode">False</property>
3203                           <property name="angle">0</property>
3204                         </widget>
3205                         <packing>
3206                           <property name="padding">0</property>
3207                           <property name="expand">False</property>
3208                           <property name="fill">False</property>
3209                         </packing>
3210                       </child>
3211                     </widget>
3212                   </child>
3213                 </widget>
3214               </child>
3215             </widget>
3216           </child>
3217
3218           <child>
3219             <widget class="GtkButton" id="UriChoiceConstantsButton">
3220               <property name="visible">True</property>
3221               <property name="sensitive">False</property>
3222               <property name="can_default">True</property>
3223               <property name="can_focus">True</property>
3224               <property name="label" translatable="yes">Try Constants</property>
3225               <property name="use_underline">True</property>
3226               <property name="relief">GTK_RELIEF_NORMAL</property>
3227               <property name="focus_on_click">True</property>
3228               <property name="response_id">0</property>
3229             </widget>
3230           </child>
3231
3232           <child>
3233             <widget class="GtkButton" id="copyButton">
3234               <property name="can_default">True</property>
3235               <property name="can_focus">True</property>
3236               <property name="label">gtk-copy</property>
3237               <property name="use_stock">True</property>
3238               <property name="relief">GTK_RELIEF_NORMAL</property>
3239               <property name="focus_on_click">True</property>
3240               <property name="response_id">0</property>
3241             </widget>
3242           </child>
3243
3244           <child>
3245             <widget class="GtkButton" id="uriChoiceAutoButton">
3246               <property name="visible">True</property>
3247               <property name="can_default">True</property>
3248               <property name="can_focus">True</property>
3249               <property name="relief">GTK_RELIEF_NORMAL</property>
3250               <property name="focus_on_click">True</property>
3251               <property name="response_id">0</property>
3252
3253               <child>
3254                 <widget class="GtkAlignment" id="alignment5">
3255                   <property name="visible">True</property>
3256                   <property name="xalign">0.5</property>
3257                   <property name="yalign">0.5</property>
3258                   <property name="xscale">0</property>
3259                   <property name="yscale">0</property>
3260                   <property name="top_padding">0</property>
3261                   <property name="bottom_padding">0</property>
3262                   <property name="left_padding">0</property>
3263                   <property name="right_padding">0</property>
3264
3265                   <child>
3266                     <widget class="GtkHBox" id="hbox16">
3267                       <property name="visible">True</property>
3268                       <property name="homogeneous">False</property>
3269                       <property name="spacing">2</property>
3270
3271                       <child>
3272                         <widget class="GtkImage" id="image302">
3273                           <property name="visible">True</property>
3274                           <property name="stock">gtk-ok</property>
3275                           <property name="icon_size">4</property>
3276                           <property name="xalign">0.5</property>
3277                           <property name="yalign">0.5</property>
3278                           <property name="xpad">0</property>
3279                           <property name="ypad">0</property>
3280                         </widget>
3281                         <packing>
3282                           <property name="padding">0</property>
3283                           <property name="expand">False</property>
3284                           <property name="fill">False</property>
3285                         </packing>
3286                       </child>
3287
3288                       <child>
3289                         <widget class="GtkLabel" id="okLabel">
3290                           <property name="visible">True</property>
3291                           <property name="label" translatable="yes">bla bla bla</property>
3292                           <property name="use_underline">True</property>
3293                           <property name="use_markup">False</property>
3294                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3295                           <property name="wrap">False</property>
3296                           <property name="selectable">False</property>
3297                           <property name="xalign">0.5</property>
3298                           <property name="yalign">0.5</property>
3299                           <property name="xpad">0</property>
3300                           <property name="ypad">0</property>
3301                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3302                           <property name="width_chars">-1</property>
3303                           <property name="single_line_mode">False</property>
3304                           <property name="angle">0</property>
3305                         </widget>
3306                         <packing>
3307                           <property name="padding">0</property>
3308                           <property name="expand">False</property>
3309                           <property name="fill">False</property>
3310                         </packing>
3311                       </child>
3312                     </widget>
3313                   </child>
3314                 </widget>
3315               </child>
3316             </widget>
3317           </child>
3318
3319           <child>
3320             <widget class="GtkButton" id="uriChoiceForwardButton">
3321               <property name="visible">True</property>
3322               <property name="can_default">True</property>
3323               <property name="can_focus">True</property>
3324               <property name="label">gtk-go-forward</property>
3325               <property name="use_stock">True</property>
3326               <property name="relief">GTK_RELIEF_NORMAL</property>
3327               <property name="focus_on_click">True</property>
3328               <property name="response_id">0</property>
3329             </widget>
3330           </child>
3331         </widget>
3332         <packing>
3333           <property name="padding">0</property>
3334           <property name="expand">False</property>
3335           <property name="fill">True</property>
3336           <property name="pack_type">GTK_PACK_END</property>
3337         </packing>
3338       </child>
3339
3340       <child>
3341         <widget class="GtkVBox" id="vbox2">
3342           <property name="visible">True</property>
3343           <property name="homogeneous">False</property>
3344           <property name="spacing">3</property>
3345
3346           <child>
3347             <widget class="GtkLabel" id="UriChoiceLabel">
3348               <property name="visible">True</property>
3349               <property name="label" translatable="yes">some informative message here ...</property>
3350               <property name="use_underline">False</property>
3351               <property name="use_markup">False</property>
3352               <property name="justify">GTK_JUSTIFY_LEFT</property>
3353               <property name="wrap">False</property>
3354               <property name="selectable">False</property>
3355               <property name="xalign">0.5</property>
3356               <property name="yalign">0.5</property>
3357               <property name="xpad">0</property>
3358               <property name="ypad">0</property>
3359               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3360               <property name="width_chars">-1</property>
3361               <property name="single_line_mode">False</property>
3362               <property name="angle">0</property>
3363             </widget>
3364             <packing>
3365               <property name="padding">0</property>
3366               <property name="expand">False</property>
3367               <property name="fill">False</property>
3368             </packing>
3369           </child>
3370
3371           <child>
3372             <widget class="GtkScrolledWindow" id="scrolledwindow1">
3373               <property name="width_request">400</property>
3374               <property name="visible">True</property>
3375               <property name="can_focus">True</property>
3376               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3377               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3378               <property name="shadow_type">GTK_SHADOW_NONE</property>
3379               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3380
3381               <child>
3382                 <widget class="GtkTreeView" id="UriChoiceTreeView">
3383                   <property name="visible">True</property>
3384                   <property name="can_focus">True</property>
3385                   <property name="headers_visible">False</property>
3386                   <property name="rules_hint">False</property>
3387                   <property name="reorderable">False</property>
3388                   <property name="enable_search">True</property>
3389                   <property name="fixed_height_mode">False</property>
3390                   <property name="hover_selection">False</property>
3391                   <property name="hover_expand">False</property>
3392                 </widget>
3393               </child>
3394             </widget>
3395             <packing>
3396               <property name="padding">0</property>
3397               <property name="expand">True</property>
3398               <property name="fill">True</property>
3399             </packing>
3400           </child>
3401
3402           <child>
3403             <widget class="GtkHBox" id="uriEntryHBox">
3404               <property name="visible">True</property>
3405               <property name="homogeneous">False</property>
3406               <property name="spacing">0</property>
3407
3408               <child>
3409                 <widget class="GtkLabel" id="label2">
3410                   <property name="visible">True</property>
3411                   <property name="label" translatable="yes">URI: </property>
3412                   <property name="use_underline">False</property>
3413                   <property name="use_markup">False</property>
3414                   <property name="justify">GTK_JUSTIFY_LEFT</property>
3415                   <property name="wrap">False</property>
3416                   <property name="selectable">False</property>
3417                   <property name="xalign">0.5</property>
3418                   <property name="yalign">0.5</property>
3419                   <property name="xpad">0</property>
3420                   <property name="ypad">0</property>
3421                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3422                   <property name="width_chars">-1</property>
3423                   <property name="single_line_mode">False</property>
3424                   <property name="angle">0</property>
3425                 </widget>
3426                 <packing>
3427                   <property name="padding">0</property>
3428                   <property name="expand">False</property>
3429                   <property name="fill">False</property>
3430                 </packing>
3431               </child>
3432
3433               <child>
3434                 <widget class="GtkEntry" id="entry1">
3435                   <property name="visible">True</property>
3436                   <property name="can_focus">True</property>
3437                   <property name="editable">True</property>
3438                   <property name="visibility">True</property>
3439                   <property name="max_length">0</property>
3440                   <property name="text" translatable="yes"></property>
3441                   <property name="has_frame">True</property>
3442                   <property name="invisible_char">*</property>
3443                   <property name="activates_default">False</property>
3444                 </widget>
3445                 <packing>
3446                   <property name="padding">0</property>
3447                   <property name="expand">True</property>
3448                   <property name="fill">True</property>
3449                 </packing>
3450               </child>
3451             </widget>
3452             <packing>
3453               <property name="padding">0</property>
3454               <property name="expand">False</property>
3455               <property name="fill">True</property>
3456             </packing>
3457           </child>
3458         </widget>
3459         <packing>
3460           <property name="padding">0</property>
3461           <property name="expand">True</property>
3462           <property name="fill">True</property>
3463         </packing>
3464       </child>
3465     </widget>
3466   </child>
3467 </widget>
3468
3469 <widget class="GtkWindow" id="FindReplWin">
3470   <property name="border_width">5</property>
3471   <property name="title" translatable="yes">Find &amp; Replace</property>
3472   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3473   <property name="window_position">GTK_WIN_POS_MOUSE</property>
3474   <property name="modal">False</property>
3475   <property name="resizable">False</property>
3476   <property name="destroy_with_parent">False</property>
3477   <property name="decorated">True</property>
3478   <property name="skip_taskbar_hint">False</property>
3479   <property name="skip_pager_hint">False</property>
3480   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3481   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3482   <property name="focus_on_map">True</property>
3483   <property name="urgency_hint">False</property>
3484
3485   <child>
3486     <widget class="GtkTable" id="table1">
3487       <property name="visible">True</property>
3488       <property name="n_rows">3</property>
3489       <property name="n_columns">2</property>
3490       <property name="homogeneous">False</property>
3491       <property name="row_spacing">5</property>
3492       <property name="column_spacing">0</property>
3493
3494       <child>
3495         <widget class="GtkLabel" id="label17">
3496           <property name="visible">True</property>
3497           <property name="label" translatable="yes">Find:</property>
3498           <property name="use_underline">False</property>
3499           <property name="use_markup">False</property>
3500           <property name="justify">GTK_JUSTIFY_LEFT</property>
3501           <property name="wrap">False</property>
3502           <property name="selectable">False</property>
3503           <property name="xalign">0</property>
3504           <property name="yalign">0.5</property>
3505           <property name="xpad">0</property>
3506           <property name="ypad">0</property>
3507           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3508           <property name="width_chars">-1</property>
3509           <property name="single_line_mode">False</property>
3510           <property name="angle">0</property>
3511         </widget>
3512         <packing>
3513           <property name="left_attach">0</property>
3514           <property name="right_attach">1</property>
3515           <property name="top_attach">0</property>
3516           <property name="bottom_attach">1</property>
3517           <property name="x_options">fill</property>
3518           <property name="y_options"></property>
3519         </packing>
3520       </child>
3521
3522       <child>
3523         <widget class="GtkLabel" id="label18">
3524           <property name="visible">True</property>
3525           <property name="label" translatable="yes">Replace with: </property>
3526           <property name="use_underline">False</property>
3527           <property name="use_markup">False</property>
3528           <property name="justify">GTK_JUSTIFY_LEFT</property>
3529           <property name="wrap">False</property>
3530           <property name="selectable">False</property>
3531           <property name="xalign">0</property>
3532           <property name="yalign">0.5</property>
3533           <property name="xpad">0</property>
3534           <property name="ypad">0</property>
3535           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3536           <property name="width_chars">-1</property>
3537           <property name="single_line_mode">False</property>
3538           <property name="angle">0</property>
3539         </widget>
3540         <packing>
3541           <property name="left_attach">0</property>
3542           <property name="right_attach">1</property>
3543           <property name="top_attach">1</property>
3544           <property name="bottom_attach">2</property>
3545           <property name="x_options">fill</property>
3546           <property name="y_options"></property>
3547         </packing>
3548       </child>
3549
3550       <child>
3551         <widget class="GtkEntry" id="findEntry">
3552           <property name="visible">True</property>
3553           <property name="can_default">True</property>
3554           <property name="has_default">True</property>
3555           <property name="can_focus">True</property>
3556           <property name="has_focus">True</property>
3557           <property name="editable">True</property>
3558           <property name="visibility">True</property>
3559           <property name="max_length">0</property>
3560           <property name="text" translatable="yes"></property>
3561           <property name="has_frame">True</property>
3562           <property name="invisible_char">*</property>
3563           <property name="activates_default">False</property>
3564         </widget>
3565         <packing>
3566           <property name="left_attach">1</property>
3567           <property name="right_attach">2</property>
3568           <property name="top_attach">0</property>
3569           <property name="bottom_attach">1</property>
3570           <property name="y_options"></property>
3571         </packing>
3572       </child>
3573
3574       <child>
3575         <widget class="GtkEntry" id="replaceEntry">
3576           <property name="visible">True</property>
3577           <property name="can_focus">True</property>
3578           <property name="editable">True</property>
3579           <property name="visibility">True</property>
3580           <property name="max_length">0</property>
3581           <property name="text" translatable="yes"></property>
3582           <property name="has_frame">True</property>
3583           <property name="invisible_char">*</property>
3584           <property name="activates_default">False</property>
3585         </widget>
3586         <packing>
3587           <property name="left_attach">1</property>
3588           <property name="right_attach">2</property>
3589           <property name="top_attach">1</property>
3590           <property name="bottom_attach">2</property>
3591           <property name="y_options"></property>
3592         </packing>
3593       </child>
3594
3595       <child>
3596         <widget class="GtkHBox" id="hbox19">
3597           <property name="visible">True</property>
3598           <property name="homogeneous">False</property>
3599           <property name="spacing">5</property>
3600
3601           <child>
3602             <widget class="GtkVBox" id="vbox9">
3603               <property name="visible">True</property>
3604               <property name="homogeneous">False</property>
3605               <property name="spacing">0</property>
3606
3607               <child>
3608                 <placeholder/>
3609               </child>
3610
3611               <child>
3612                 <placeholder/>
3613               </child>
3614             </widget>
3615             <packing>
3616               <property name="padding">0</property>
3617               <property name="expand">True</property>
3618               <property name="fill">True</property>
3619             </packing>
3620           </child>
3621
3622           <child>
3623             <widget class="GtkButton" id="findButton">
3624               <property name="visible">True</property>
3625               <property name="can_focus">True</property>
3626               <property name="label">gtk-find</property>
3627               <property name="use_stock">True</property>
3628               <property name="relief">GTK_RELIEF_NORMAL</property>
3629               <property name="focus_on_click">True</property>
3630             </widget>
3631             <packing>
3632               <property name="padding">0</property>
3633               <property name="expand">False</property>
3634               <property name="fill">False</property>
3635             </packing>
3636           </child>
3637
3638           <child>
3639             <widget class="GtkButton" id="findReplButton">
3640               <property name="visible">True</property>
3641               <property name="can_focus">True</property>
3642               <property name="relief">GTK_RELIEF_NORMAL</property>
3643               <property name="focus_on_click">True</property>
3644
3645               <child>
3646                 <widget class="GtkAlignment" id="alignment13">
3647                   <property name="visible">True</property>
3648                   <property name="xalign">0.5</property>
3649                   <property name="yalign">0.5</property>
3650                   <property name="xscale">0</property>
3651                   <property name="yscale">0</property>
3652                   <property name="top_padding">0</property>
3653                   <property name="bottom_padding">0</property>
3654                   <property name="left_padding">0</property>
3655                   <property name="right_padding">0</property>
3656
3657                   <child>
3658                     <widget class="GtkHBox" id="hbox20">
3659                       <property name="visible">True</property>
3660                       <property name="homogeneous">False</property>
3661                       <property name="spacing">2</property>
3662
3663                       <child>
3664                         <widget class="GtkImage" id="image357">
3665                           <property name="visible">True</property>
3666                           <property name="stock">gtk-find-and-replace</property>
3667                           <property name="icon_size">4</property>
3668                           <property name="xalign">0.5</property>
3669                           <property name="yalign">0.5</property>
3670                           <property name="xpad">0</property>
3671                           <property name="ypad">0</property>
3672                         </widget>
3673                         <packing>
3674                           <property name="padding">0</property>
3675                           <property name="expand">False</property>
3676                           <property name="fill">False</property>
3677                         </packing>
3678                       </child>
3679
3680                       <child>
3681                         <widget class="GtkLabel" id="label19">
3682                           <property name="visible">True</property>
3683                           <property name="label">_Replace</property>
3684                           <property name="use_underline">True</property>
3685                           <property name="use_markup">False</property>
3686                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3687                           <property name="wrap">False</property>
3688                           <property name="selectable">False</property>
3689                           <property name="xalign">0.5</property>
3690                           <property name="yalign">0.5</property>
3691                           <property name="xpad">0</property>
3692                           <property name="ypad">0</property>
3693                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3694                           <property name="width_chars">-1</property>
3695                           <property name="single_line_mode">False</property>
3696                           <property name="angle">0</property>
3697                         </widget>
3698                         <packing>
3699                           <property name="padding">0</property>
3700                           <property name="expand">False</property>
3701                           <property name="fill">False</property>
3702                         </packing>
3703                       </child>
3704                     </widget>
3705                   </child>
3706                 </widget>
3707               </child>
3708             </widget>
3709             <packing>
3710               <property name="padding">0</property>
3711               <property name="expand">False</property>
3712               <property name="fill">False</property>
3713             </packing>
3714           </child>
3715
3716           <child>
3717             <widget class="GtkButton" id="cancelButton">
3718               <property name="visible">True</property>
3719               <property name="can_focus">True</property>
3720               <property name="label">gtk-cancel</property>
3721               <property name="use_stock">True</property>
3722               <property name="relief">GTK_RELIEF_NORMAL</property>
3723               <property name="focus_on_click">True</property>
3724             </widget>
3725             <packing>
3726               <property name="padding">0</property>
3727               <property name="expand">False</property>
3728               <property name="fill">False</property>
3729             </packing>
3730           </child>
3731         </widget>
3732         <packing>
3733           <property name="left_attach">0</property>
3734           <property name="right_attach">2</property>
3735           <property name="top_attach">2</property>
3736           <property name="bottom_attach">3</property>
3737           <property name="y_padding">5</property>
3738         </packing>
3739       </child>
3740     </widget>
3741   </child>
3742 </widget>
3743
3744 <widget class="GtkWindow" id="NewDevelWin">
3745   <property name="title" translatable="yes">Create development</property>
3746   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3747   <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
3748   <property name="modal">True</property>
3749   <property name="resizable">False</property>
3750   <property name="destroy_with_parent">False</property>
3751   <property name="decorated">True</property>
3752   <property name="skip_taskbar_hint">False</property>
3753   <property name="skip_pager_hint">False</property>
3754   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
3755   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3756   <property name="focus_on_map">True</property>
3757   <property name="urgency_hint">False</property>
3758
3759   <child>
3760     <widget class="GtkVBox" id="vbox10">
3761       <property name="visible">True</property>
3762       <property name="homogeneous">False</property>
3763       <property name="spacing">0</property>
3764
3765       <child>
3766         <widget class="GtkTable" id="table2">
3767           <property name="border_width">3</property>
3768           <property name="visible">True</property>
3769           <property name="n_rows">2</property>
3770           <property name="n_columns">3</property>
3771           <property name="homogeneous">False</property>
3772           <property name="row_spacing">5</property>
3773           <property name="column_spacing">5</property>
3774
3775           <child>
3776             <widget class="GtkLabel" id="label20">
3777               <property name="visible">True</property>
3778               <property name="label" translatable="yes">Name</property>
3779               <property name="use_underline">False</property>
3780               <property name="use_markup">False</property>
3781               <property name="justify">GTK_JUSTIFY_LEFT</property>
3782               <property name="wrap">False</property>
3783               <property name="selectable">False</property>
3784               <property name="xalign">0</property>
3785               <property name="yalign">0.5</property>
3786               <property name="xpad">0</property>
3787               <property name="ypad">0</property>
3788               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3789               <property name="width_chars">-1</property>
3790               <property name="single_line_mode">False</property>
3791               <property name="angle">0</property>
3792             </widget>
3793             <packing>
3794               <property name="left_attach">0</property>
3795               <property name="right_attach">1</property>
3796               <property name="top_attach">0</property>
3797               <property name="bottom_attach">1</property>
3798               <property name="x_options">fill</property>
3799               <property name="y_options"></property>
3800             </packing>
3801           </child>
3802
3803           <child>
3804             <widget class="GtkLabel" id="label21">
3805               <property name="visible">True</property>
3806               <property name="label" translatable="yes">Root directory</property>
3807               <property name="use_underline">False</property>
3808               <property name="use_markup">False</property>
3809               <property name="justify">GTK_JUSTIFY_LEFT</property>
3810               <property name="wrap">False</property>
3811               <property name="selectable">False</property>
3812               <property name="xalign">0</property>
3813               <property name="yalign">0.5</property>
3814               <property name="xpad">0</property>
3815               <property name="ypad">0</property>
3816               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3817               <property name="width_chars">-1</property>
3818               <property name="single_line_mode">False</property>
3819               <property name="angle">0</property>
3820             </widget>
3821             <packing>
3822               <property name="left_attach">0</property>
3823               <property name="right_attach">1</property>
3824               <property name="top_attach">1</property>
3825               <property name="bottom_attach">2</property>
3826               <property name="x_options">fill</property>
3827               <property name="y_options"></property>
3828             </packing>
3829           </child>
3830
3831           <child>
3832             <widget class="GtkEntry" id="nameEntry">
3833               <property name="visible">True</property>
3834               <property name="can_focus">True</property>
3835               <property name="editable">True</property>
3836               <property name="visibility">True</property>
3837               <property name="max_length">0</property>
3838               <property name="text" translatable="yes"></property>
3839               <property name="has_frame">True</property>
3840               <property name="invisible_char">*</property>
3841               <property name="activates_default">False</property>
3842             </widget>
3843             <packing>
3844               <property name="left_attach">1</property>
3845               <property name="right_attach">2</property>
3846               <property name="top_attach">0</property>
3847               <property name="bottom_attach">1</property>
3848               <property name="y_options"></property>
3849             </packing>
3850           </child>
3851
3852           <child>
3853             <widget class="GtkEntry" id="rootEntry">
3854               <property name="visible">True</property>
3855               <property name="can_focus">True</property>
3856               <property name="editable">True</property>
3857               <property name="visibility">True</property>
3858               <property name="max_length">0</property>
3859               <property name="text" translatable="yes"></property>
3860               <property name="has_frame">True</property>
3861               <property name="invisible_char">*</property>
3862               <property name="activates_default">False</property>
3863             </widget>
3864             <packing>
3865               <property name="left_attach">1</property>
3866               <property name="right_attach">2</property>
3867               <property name="top_attach">1</property>
3868               <property name="bottom_attach">2</property>
3869               <property name="y_options"></property>
3870             </packing>
3871           </child>
3872
3873           <child>
3874             <widget class="GtkButton" id="chooseRootButton">
3875               <property name="visible">True</property>
3876               <property name="can_focus">True</property>
3877               <property name="label" translatable="yes">...</property>
3878               <property name="use_underline">True</property>
3879               <property name="relief">GTK_RELIEF_NORMAL</property>
3880               <property name="focus_on_click">True</property>
3881             </widget>
3882             <packing>
3883               <property name="left_attach">2</property>
3884               <property name="right_attach">3</property>
3885               <property name="top_attach">1</property>
3886               <property name="bottom_attach">2</property>
3887               <property name="x_options">fill</property>
3888               <property name="y_options"></property>
3889             </packing>
3890           </child>
3891         </widget>
3892         <packing>
3893           <property name="padding">0</property>
3894           <property name="expand">False</property>
3895           <property name="fill">True</property>
3896         </packing>
3897       </child>
3898
3899       <child>
3900         <widget class="GtkHSeparator" id="hseparator1">
3901           <property name="visible">True</property>
3902         </widget>
3903         <packing>
3904           <property name="padding">2</property>
3905           <property name="expand">False</property>
3906           <property name="fill">True</property>
3907         </packing>
3908       </child>
3909
3910       <child>
3911         <widget class="GtkHBox" id="hbox21">
3912           <property name="border_width">3</property>
3913           <property name="visible">True</property>
3914           <property name="homogeneous">False</property>
3915           <property name="spacing">5</property>
3916
3917           <child>
3918             <widget class="GtkVBox" id="vbox11">
3919               <property name="visible">True</property>
3920               <property name="homogeneous">False</property>
3921               <property name="spacing">0</property>
3922
3923               <child>
3924                 <placeholder/>
3925               </child>
3926
3927               <child>
3928                 <placeholder/>
3929               </child>
3930             </widget>
3931             <packing>
3932               <property name="padding">0</property>
3933               <property name="expand">True</property>
3934               <property name="fill">True</property>
3935             </packing>
3936           </child>
3937
3938           <child>
3939             <widget class="GtkButton" id="addButton">
3940               <property name="visible">True</property>
3941               <property name="can_focus">True</property>
3942               <property name="label">gtk-add</property>
3943               <property name="use_stock">True</property>
3944               <property name="relief">GTK_RELIEF_NORMAL</property>
3945               <property name="focus_on_click">True</property>
3946             </widget>
3947             <packing>
3948               <property name="padding">0</property>
3949               <property name="expand">False</property>
3950               <property name="fill">False</property>
3951             </packing>
3952           </child>
3953
3954           <child>
3955             <widget class="GtkButton" id="cancelButton">
3956               <property name="visible">True</property>
3957               <property name="can_focus">True</property>
3958               <property name="label">gtk-cancel</property>
3959               <property name="use_stock">True</property>
3960               <property name="relief">GTK_RELIEF_NORMAL</property>
3961               <property name="focus_on_click">True</property>
3962             </widget>
3963             <packing>
3964               <property name="padding">0</property>
3965               <property name="expand">False</property>
3966               <property name="fill">False</property>
3967             </packing>
3968           </child>
3969         </widget>
3970         <packing>
3971           <property name="padding">0</property>
3972           <property name="expand">False</property>
3973           <property name="fill">True</property>
3974         </packing>
3975       </child>
3976     </widget>
3977   </child>
3978 </widget>
3979
3980 <widget class="GtkWindow" id="DevelListWin">
3981   <property name="title" translatable="yes">Developments</property>
3982   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3983   <property name="window_position">GTK_WIN_POS_CENTER</property>
3984   <property name="modal">False</property>
3985   <property name="resizable">True</property>
3986   <property name="destroy_with_parent">False</property>
3987   <property name="decorated">True</property>
3988   <property name="skip_taskbar_hint">False</property>
3989   <property name="skip_pager_hint">False</property>
3990   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
3991   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3992   <property name="focus_on_map">True</property>
3993   <property name="urgency_hint">False</property>
3994
3995   <child>
3996     <widget class="GtkVBox" id="vbox12">
3997       <property name="visible">True</property>
3998       <property name="homogeneous">False</property>
3999       <property name="spacing">0</property>
4000
4001       <child>
4002         <widget class="GtkScrolledWindow" id="scrolledwindow10">
4003           <property name="visible">True</property>
4004           <property name="can_focus">True</property>
4005           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4006           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4007           <property name="shadow_type">GTK_SHADOW_IN</property>
4008           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
4009
4010           <child>
4011             <widget class="GtkTreeView" id="developmentsTreeview">
4012               <property name="visible">True</property>
4013               <property name="can_focus">True</property>
4014               <property name="headers_visible">False</property>
4015               <property name="rules_hint">False</property>
4016               <property name="reorderable">False</property>
4017               <property name="enable_search">True</property>
4018               <property name="fixed_height_mode">False</property>
4019               <property name="hover_selection">False</property>
4020               <property name="hover_expand">False</property>
4021             </widget>
4022           </child>
4023         </widget>
4024         <packing>
4025           <property name="padding">0</property>
4026           <property name="expand">True</property>
4027           <property name="fill">True</property>
4028         </packing>
4029       </child>
4030
4031       <child>
4032         <widget class="GtkHSeparator" id="hseparator2">
4033           <property name="visible">True</property>
4034         </widget>
4035         <packing>
4036           <property name="padding">2</property>
4037           <property name="expand">False</property>
4038           <property name="fill">True</property>
4039         </packing>
4040       </child>
4041
4042       <child>
4043         <widget class="GtkHBox" id="buttonsHbox">
4044           <property name="border_width">3</property>
4045           <property name="visible">True</property>
4046           <property name="homogeneous">False</property>
4047           <property name="spacing">4</property>
4048
4049           <child>
4050             <widget class="GtkVBox" id="vbox13">
4051               <property name="visible">True</property>
4052               <property name="homogeneous">False</property>
4053               <property name="spacing">0</property>
4054
4055               <child>
4056                 <placeholder/>
4057               </child>
4058
4059               <child>
4060                 <placeholder/>
4061               </child>
4062             </widget>
4063             <packing>
4064               <property name="padding">0</property>
4065               <property name="expand">True</property>
4066               <property name="fill">True</property>
4067             </packing>
4068           </child>
4069
4070           <child>
4071             <widget class="GtkButton" id="newButton">
4072               <property name="visible">True</property>
4073               <property name="can_focus">True</property>
4074               <property name="label">gtk-new</property>
4075               <property name="use_stock">True</property>
4076               <property name="relief">GTK_RELIEF_NORMAL</property>
4077               <property name="focus_on_click">True</property>
4078             </widget>
4079             <packing>
4080               <property name="padding">0</property>
4081               <property name="expand">False</property>
4082               <property name="fill">False</property>
4083             </packing>
4084           </child>
4085
4086           <child>
4087             <widget class="GtkButton" id="deleteButton">
4088               <property name="visible">True</property>
4089               <property name="can_focus">True</property>
4090               <property name="label">gtk-delete</property>
4091               <property name="use_stock">True</property>
4092               <property name="relief">GTK_RELIEF_NORMAL</property>
4093               <property name="focus_on_click">True</property>
4094             </widget>
4095             <packing>
4096               <property name="padding">0</property>
4097               <property name="expand">False</property>
4098               <property name="fill">False</property>
4099             </packing>
4100           </child>
4101
4102           <child>
4103             <widget class="GtkButton" id="buildButton">
4104               <property name="visible">True</property>
4105               <property name="can_focus">True</property>
4106               <property name="relief">GTK_RELIEF_NORMAL</property>
4107               <property name="focus_on_click">True</property>
4108
4109               <child>
4110                 <widget class="GtkAlignment" id="alignment14">
4111                   <property name="visible">True</property>
4112                   <property name="xalign">0.5</property>
4113                   <property name="yalign">0.5</property>
4114                   <property name="xscale">0</property>
4115                   <property name="yscale">0</property>
4116                   <property name="top_padding">0</property>
4117                   <property name="bottom_padding">0</property>
4118                   <property name="left_padding">0</property>
4119                   <property name="right_padding">0</property>
4120
4121                   <child>
4122                     <widget class="GtkHBox" id="hbox23">
4123                       <property name="visible">True</property>
4124                       <property name="homogeneous">False</property>
4125                       <property name="spacing">2</property>
4126
4127                       <child>
4128                         <widget class="GtkImage" id="image358">
4129                           <property name="visible">True</property>
4130                           <property name="stock">gtk-execute</property>
4131                           <property name="icon_size">4</property>
4132                           <property name="xalign">0.5</property>
4133                           <property name="yalign">0.5</property>
4134                           <property name="xpad">0</property>
4135                           <property name="ypad">0</property>
4136                         </widget>
4137                         <packing>
4138                           <property name="padding">0</property>
4139                           <property name="expand">False</property>
4140                           <property name="fill">False</property>
4141                         </packing>
4142                       </child>
4143
4144                       <child>
4145                         <widget class="GtkLabel" id="label22">
4146                           <property name="visible">True</property>
4147                           <property name="label" translatable="yes">_Build</property>
4148                           <property name="use_underline">True</property>
4149                           <property name="use_markup">False</property>
4150                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4151                           <property name="wrap">False</property>
4152                           <property name="selectable">False</property>
4153                           <property name="xalign">0.5</property>
4154                           <property name="yalign">0.5</property>
4155                           <property name="xpad">0</property>
4156                           <property name="ypad">0</property>
4157                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4158                           <property name="width_chars">-1</property>
4159                           <property name="single_line_mode">False</property>
4160                           <property name="angle">0</property>
4161                         </widget>
4162                         <packing>
4163                           <property name="padding">0</property>
4164                           <property name="expand">False</property>
4165                           <property name="fill">False</property>
4166                         </packing>
4167                       </child>
4168                     </widget>
4169                   </child>
4170                 </widget>
4171               </child>
4172             </widget>
4173             <packing>
4174               <property name="padding">0</property>
4175               <property name="expand">False</property>
4176               <property name="fill">False</property>
4177             </packing>
4178           </child>
4179
4180           <child>
4181             <widget class="GtkButton" id="cleanButton">
4182               <property name="visible">True</property>
4183               <property name="can_focus">True</property>
4184               <property name="relief">GTK_RELIEF_NORMAL</property>
4185               <property name="focus_on_click">True</property>
4186
4187               <child>
4188                 <widget class="GtkAlignment" id="alignment15">
4189                   <property name="visible">True</property>
4190                   <property name="xalign">0.5</property>
4191                   <property name="yalign">0.5</property>
4192                   <property name="xscale">0</property>
4193                   <property name="yscale">0</property>
4194                   <property name="top_padding">0</property>
4195                   <property name="bottom_padding">0</property>
4196                   <property name="left_padding">0</property>
4197                   <property name="right_padding">0</property>
4198
4199                   <child>
4200                     <widget class="GtkHBox" id="hbox24">
4201                       <property name="visible">True</property>
4202                       <property name="homogeneous">False</property>
4203                       <property name="spacing">2</property>
4204
4205                       <child>
4206                         <widget class="GtkImage" id="image359">
4207                           <property name="visible">True</property>
4208                           <property name="stock">gtk-clear</property>
4209                           <property name="icon_size">4</property>
4210                           <property name="xalign">0.5</property>
4211                           <property name="yalign">0.5</property>
4212                           <property name="xpad">0</property>
4213                           <property name="ypad">0</property>
4214                         </widget>
4215                         <packing>
4216                           <property name="padding">0</property>
4217                           <property name="expand">False</property>
4218                           <property name="fill">False</property>
4219                         </packing>
4220                       </child>
4221
4222                       <child>
4223                         <widget class="GtkLabel" id="label23">
4224                           <property name="visible">True</property>
4225                           <property name="label" translatable="yes">C_lean</property>
4226                           <property name="use_underline">True</property>
4227                           <property name="use_markup">False</property>
4228                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4229                           <property name="wrap">False</property>
4230                           <property name="selectable">False</property>
4231                           <property name="xalign">0.5</property>
4232                           <property name="yalign">0.5</property>
4233                           <property name="xpad">0</property>
4234                           <property name="ypad">0</property>
4235                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4236                           <property name="width_chars">-1</property>
4237                           <property name="single_line_mode">False</property>
4238                           <property name="angle">0</property>
4239                         </widget>
4240                         <packing>
4241                           <property name="padding">0</property>
4242                           <property name="expand">False</property>
4243                           <property name="fill">False</property>
4244                         </packing>
4245                       </child>
4246                     </widget>
4247                   </child>
4248                 </widget>
4249               </child>
4250             </widget>
4251             <packing>
4252               <property name="padding">0</property>
4253               <property name="expand">False</property>
4254               <property name="fill">False</property>
4255             </packing>
4256           </child>
4257
4258           <child>
4259             <widget class="GtkButton" id="publishButton">
4260               <property name="visible">True</property>
4261               <property name="can_focus">True</property>
4262               <property name="relief">GTK_RELIEF_NORMAL</property>
4263               <property name="focus_on_click">True</property>
4264
4265               <child>
4266                 <widget class="GtkAlignment" id="alignment16">
4267                   <property name="visible">True</property>
4268                   <property name="xalign">0.5</property>
4269                   <property name="yalign">0.5</property>
4270                   <property name="xscale">0</property>
4271                   <property name="yscale">0</property>
4272                   <property name="top_padding">0</property>
4273                   <property name="bottom_padding">0</property>
4274                   <property name="left_padding">0</property>
4275                   <property name="right_padding">0</property>
4276
4277                   <child>
4278                     <widget class="GtkHBox" id="hbox25">
4279                       <property name="visible">True</property>
4280                       <property name="homogeneous">False</property>
4281                       <property name="spacing">2</property>
4282
4283                       <child>
4284                         <widget class="GtkImage" id="image907">
4285                           <property name="visible">True</property>
4286                           <property name="stock">gtk-convert</property>
4287                           <property name="icon_size">4</property>
4288                           <property name="xalign">0.5</property>
4289                           <property name="yalign">0.5</property>
4290                           <property name="xpad">0</property>
4291                           <property name="ypad">0</property>
4292                         </widget>
4293                         <packing>
4294                           <property name="padding">0</property>
4295                           <property name="expand">False</property>
4296                           <property name="fill">False</property>
4297                         </packing>
4298                       </child>
4299
4300                       <child>
4301                         <widget class="GtkLabel" id="label24">
4302                           <property name="visible">True</property>
4303                           <property name="label" translatable="yes">Publish</property>
4304                           <property name="use_underline">True</property>
4305                           <property name="use_markup">False</property>
4306                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4307                           <property name="wrap">False</property>
4308                           <property name="selectable">False</property>
4309                           <property name="xalign">0.5</property>
4310                           <property name="yalign">0.5</property>
4311                           <property name="xpad">0</property>
4312                           <property name="ypad">0</property>
4313                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4314                           <property name="width_chars">-1</property>
4315                           <property name="single_line_mode">False</property>
4316                           <property name="angle">0</property>
4317                         </widget>
4318                         <packing>
4319                           <property name="padding">0</property>
4320                           <property name="expand">False</property>
4321                           <property name="fill">False</property>
4322                         </packing>
4323                       </child>
4324                     </widget>
4325                   </child>
4326                 </widget>
4327               </child>
4328             </widget>
4329             <packing>
4330               <property name="padding">0</property>
4331               <property name="expand">False</property>
4332               <property name="fill">False</property>
4333             </packing>
4334           </child>
4335
4336           <child>
4337             <widget class="GtkButton" id="graphButton">
4338               <property name="visible">True</property>
4339               <property name="can_focus">True</property>
4340               <property name="relief">GTK_RELIEF_NORMAL</property>
4341               <property name="focus_on_click">True</property>
4342
4343               <child>
4344                 <widget class="GtkAlignment" id="alignment17">
4345                   <property name="visible">True</property>
4346                   <property name="xalign">0.5</property>
4347                   <property name="yalign">0.5</property>
4348                   <property name="xscale">0</property>
4349                   <property name="yscale">0</property>
4350                   <property name="top_padding">0</property>
4351                   <property name="bottom_padding">0</property>
4352                   <property name="left_padding">0</property>
4353                   <property name="right_padding">0</property>
4354
4355                   <child>
4356                     <widget class="GtkHBox" id="hbox26">
4357                       <property name="visible">True</property>
4358                       <property name="homogeneous">False</property>
4359                       <property name="spacing">2</property>
4360
4361                       <child>
4362                         <widget class="GtkImage" id="image908">
4363                           <property name="visible">True</property>
4364                           <property name="stock">gtk-zoom-fit</property>
4365                           <property name="icon_size">4</property>
4366                           <property name="xalign">0.5</property>
4367                           <property name="yalign">0.5</property>
4368                           <property name="xpad">0</property>
4369                           <property name="ypad">0</property>
4370                         </widget>
4371                         <packing>
4372                           <property name="padding">0</property>
4373                           <property name="expand">False</property>
4374                           <property name="fill">False</property>
4375                         </packing>
4376                       </child>
4377
4378                       <child>
4379                         <widget class="GtkLabel" id="label27">
4380                           <property name="visible">True</property>
4381                           <property name="label" translatable="yes">Graph</property>
4382                           <property name="use_underline">True</property>
4383                           <property name="use_markup">False</property>
4384                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4385                           <property name="wrap">False</property>
4386                           <property name="selectable">False</property>
4387                           <property name="xalign">0.5</property>
4388                           <property name="yalign">0.5</property>
4389                           <property name="xpad">0</property>
4390                           <property name="ypad">0</property>
4391                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4392                           <property name="width_chars">-1</property>
4393                           <property name="single_line_mode">False</property>
4394                           <property name="angle">0</property>
4395                         </widget>
4396                         <packing>
4397                           <property name="padding">0</property>
4398                           <property name="expand">False</property>
4399                           <property name="fill">False</property>
4400                         </packing>
4401                       </child>
4402                     </widget>
4403                   </child>
4404                 </widget>
4405               </child>
4406             </widget>
4407             <packing>
4408               <property name="padding">0</property>
4409               <property name="expand">False</property>
4410               <property name="fill">False</property>
4411             </packing>
4412           </child>
4413
4414           <child>
4415             <widget class="GtkButton" id="closeButton">
4416               <property name="visible">True</property>
4417               <property name="can_focus">True</property>
4418               <property name="label">gtk-close</property>
4419               <property name="use_stock">True</property>
4420               <property name="relief">GTK_RELIEF_NORMAL</property>
4421               <property name="focus_on_click">True</property>
4422             </widget>
4423             <packing>
4424               <property name="padding">0</property>
4425               <property name="expand">False</property>
4426               <property name="fill">False</property>
4427             </packing>
4428           </child>
4429         </widget>
4430         <packing>
4431           <property name="padding">0</property>
4432           <property name="expand">False</property>
4433           <property name="fill">True</property>
4434         </packing>
4435       </child>
4436     </widget>
4437   </child>
4438 </widget>
4439
4440 <widget class="GtkDialog" id="DisambiguationErrors">
4441   <property name="width_request">450</property>
4442   <property name="height_request">400</property>
4443   <property name="title" translatable="yes">title</property>
4444   <property name="type">GTK_WINDOW_TOPLEVEL</property>
4445   <property name="window_position">GTK_WIN_POS_NONE</property>
4446   <property name="modal">True</property>
4447   <property name="resizable">True</property>
4448   <property name="destroy_with_parent">False</property>
4449   <property name="decorated">True</property>
4450   <property name="skip_taskbar_hint">False</property>
4451   <property name="skip_pager_hint">False</property>
4452   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
4453   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
4454   <property name="focus_on_map">True</property>
4455   <property name="urgency_hint">False</property>
4456   <property name="has_separator">True</property>
4457
4458   <child internal-child="vbox">
4459     <widget class="GtkVBox" id="vbox14">
4460       <property name="visible">True</property>
4461       <property name="homogeneous">False</property>
4462       <property name="spacing">0</property>
4463
4464       <child internal-child="action_area">
4465         <widget class="GtkHButtonBox" id="hbuttonbox2">
4466           <property name="visible">True</property>
4467           <property name="layout_style">GTK_BUTTONBOX_END</property>
4468
4469           <child>
4470             <widget class="GtkButton" id="button6">
4471               <property name="visible">True</property>
4472               <property name="can_default">True</property>
4473               <property name="can_focus">True</property>
4474               <property name="label">gtk-help</property>
4475               <property name="use_stock">True</property>
4476               <property name="relief">GTK_RELIEF_NORMAL</property>
4477               <property name="focus_on_click">True</property>
4478               <property name="response_id">-11</property>
4479             </widget>
4480           </child>
4481
4482           <child>
4483             <widget class="GtkButton" id="disambiguationErrorsMoreErrors">
4484               <property name="visible">True</property>
4485               <property name="can_default">True</property>
4486               <property name="can_focus">True</property>
4487               <property name="relief">GTK_RELIEF_NORMAL</property>
4488               <property name="focus_on_click">True</property>
4489               <property name="response_id">-6</property>
4490
4491               <child>
4492                 <widget class="GtkAlignment" id="alignment18">
4493                   <property name="visible">True</property>
4494                   <property name="xalign">0.5</property>
4495                   <property name="yalign">0.5</property>
4496                   <property name="xscale">0</property>
4497                   <property name="yscale">0</property>
4498                   <property name="top_padding">0</property>
4499                   <property name="bottom_padding">0</property>
4500                   <property name="left_padding">0</property>
4501                   <property name="right_padding">0</property>
4502
4503                   <child>
4504                     <widget class="GtkHBox" id="hbox29">
4505                       <property name="visible">True</property>
4506                       <property name="homogeneous">False</property>
4507                       <property name="spacing">2</property>
4508
4509                       <child>
4510                         <widget class="GtkImage" id="image926">
4511                           <property name="visible">True</property>
4512                           <property name="stock">gtk-zoom-in</property>
4513                           <property name="icon_size">4</property>
4514                           <property name="xalign">0.5</property>
4515                           <property name="yalign">0.5</property>
4516                           <property name="xpad">0</property>
4517                           <property name="ypad">0</property>
4518                         </widget>
4519                         <packing>
4520                           <property name="padding">0</property>
4521                           <property name="expand">False</property>
4522                           <property name="fill">False</property>
4523                         </packing>
4524                       </child>
4525
4526                       <child>
4527                         <widget class="GtkLabel" id="label28">
4528                           <property name="visible">True</property>
4529                           <property name="label">More</property>
4530                           <property name="use_underline">True</property>
4531                           <property name="use_markup">False</property>
4532                           <property name="justify">GTK_JUSTIFY_LEFT</property>
4533                           <property name="wrap">False</property>
4534                           <property name="selectable">False</property>
4535                           <property name="xalign">0.5</property>
4536                           <property name="yalign">0.5</property>
4537                           <property name="xpad">0</property>
4538                           <property name="ypad">0</property>
4539                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4540                           <property name="width_chars">-1</property>
4541                           <property name="single_line_mode">False</property>
4542                           <property name="angle">0</property>
4543                         </widget>
4544                         <packing>
4545                           <property name="padding">0</property>
4546                           <property name="expand">False</property>
4547                           <property name="fill">False</property>
4548                         </packing>
4549                       </child>
4550                     </widget>
4551                   </child>
4552                 </widget>
4553               </child>
4554             </widget>
4555           </child>
4556
4557           <child>
4558             <widget class="GtkButton" id="disambiguationErrorsCancelButton">
4559               <property name="visible">True</property>
4560               <property name="can_default">True</property>
4561               <property name="has_default">True</property>
4562               <property name="can_focus">True</property>
4563               <property name="label">gtk-cancel</property>
4564               <property name="use_stock">True</property>
4565               <property name="relief">GTK_RELIEF_NORMAL</property>
4566               <property name="focus_on_click">True</property>
4567               <property name="response_id">-6</property>
4568             </widget>
4569           </child>
4570
4571           <child>
4572             <widget class="GtkButton" id="disambiguationErrorsOkButton">
4573               <property name="visible">True</property>
4574               <property name="can_default">True</property>
4575               <property name="can_focus">True</property>
4576               <property name="label">gtk-ok</property>
4577               <property name="use_stock">True</property>
4578               <property name="relief">GTK_RELIEF_NORMAL</property>
4579               <property name="focus_on_click">True</property>
4580               <property name="response_id">-5</property>
4581             </widget>
4582           </child>
4583         </widget>
4584         <packing>
4585           <property name="padding">0</property>
4586           <property name="expand">False</property>
4587           <property name="fill">True</property>
4588           <property name="pack_type">GTK_PACK_END</property>
4589         </packing>
4590       </child>
4591
4592       <child>
4593         <widget class="GtkVBox" id="vbox15">
4594           <property name="visible">True</property>
4595           <property name="homogeneous">False</property>
4596           <property name="spacing">0</property>
4597
4598           <child>
4599             <widget class="GtkLabel" id="disambiguationErrorsLabel">
4600               <property name="visible">True</property>
4601               <property name="label" translatable="yes">some informative message here ...</property>
4602               <property name="use_underline">False</property>
4603               <property name="use_markup">False</property>
4604               <property name="justify">GTK_JUSTIFY_LEFT</property>
4605               <property name="wrap">False</property>
4606               <property name="selectable">False</property>
4607               <property name="xalign">0.5</property>
4608               <property name="yalign">0.5</property>
4609               <property name="xpad">0</property>
4610               <property name="ypad">0</property>
4611               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
4612               <property name="width_chars">-1</property>
4613               <property name="single_line_mode">False</property>
4614               <property name="angle">0</property>
4615             </widget>
4616             <packing>
4617               <property name="padding">0</property>
4618               <property name="expand">False</property>
4619               <property name="fill">False</property>
4620             </packing>
4621           </child>
4622
4623           <child>
4624             <widget class="GtkScrolledWindow" id="scrolledwindow12">
4625               <property name="visible">True</property>
4626               <property name="can_focus">True</property>
4627               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4628               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
4629               <property name="shadow_type">GTK_SHADOW_IN</property>
4630               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
4631
4632               <child>
4633                 <widget class="GtkTreeView" id="treeview">
4634                   <property name="visible">True</property>
4635                   <property name="can_focus">True</property>
4636                   <property name="headers_visible">False</property>
4637                   <property name="rules_hint">False</property>
4638                   <property name="reorderable">False</property>
4639                   <property name="enable_search">True</property>
4640                   <property name="fixed_height_mode">False</property>
4641                   <property name="hover_selection">False</property>
4642                   <property name="hover_expand">False</property>
4643                 </widget>
4644               </child>
4645             </widget>
4646             <packing>
4647               <property name="padding">0</property>
4648               <property name="expand">True</property>
4649               <property name="fill">True</property>
4650             </packing>
4651           </child>
4652         </widget>
4653         <packing>
4654           <property name="padding">0</property>
4655           <property name="expand">True</property>
4656           <property name="fill">True</property>
4657         </packing>
4658       </child>
4659     </widget>
4660   </child>
4661 </widget>
4662
4663 </glade-interface>