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