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