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="image712">
 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="image713">
 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="image714">
 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="image715">
 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="image716">
 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="image717">
 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="image718">
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="image719">
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="image720">
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="image721">
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="image722">
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="image723">
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="image724">
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="viewMenu">
1220                       <property name="visible">True</property>
1221                       <property name="label" translatable="yes">_View</property>
1222                       <property name="use_underline">True</property>
1223
1224                       <child>
1225                         <widget class="GtkMenu" id="viewMenu_menu">
1226
1227                           <child>
1228                             <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
1229                               <property name="visible">True</property>
1230                               <property name="label" translatable="yes">Show _Tactics Bar</property>
1231                               <property name="use_underline">True</property>
1232                               <property name="active">True</property>
1233                               <accelerator key="F2" modifiers="0" signal="activate"/>
1234                             </widget>
1235                           </child>
1236
1237                           <child>
1238                             <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1239                               <property name="visible">True</property>
1240                               <property name="label" translatable="yes">New Cic _Browser</property>
1241                               <property name="use_underline">True</property>
1242                               <accelerator key="F3" modifiers="0" signal="activate"/>
1243                             </widget>
1244                           </child>
1245
1246                           <child>
1247                             <widget class="GtkSeparatorMenuItem" id="separator5">
1248                               <property name="visible">True</property>
1249                             </widget>
1250                           </child>
1251
1252                           <child>
1253                             <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1254                               <property name="visible">True</property>
1255                               <property name="label" translatable="yes">_Fullscreen</property>
1256                               <property name="use_underline">True</property>
1257                               <property name="active">False</property>
1258                               <accelerator key="F11" modifiers="0" signal="activate"/>
1259                             </widget>
1260                           </child>
1261
1262                           <child>
1263                             <widget class="GtkSeparatorMenuItem" id="separator1">
1264                               <property name="visible">True</property>
1265                             </widget>
1266                           </child>
1267
1268                           <child>
1269                             <widget class="GtkImageMenuItem" id="increaseFontSizeMenuItem">
1270                               <property name="visible">True</property>
1271                               <property name="label" translatable="yes">Zoom _In</property>
1272                               <property name="use_underline">True</property>
1273                               <signal name="activate" handler="on_increaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1274                               <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1275
1276                               <child internal-child="image">
1277                                 <widget class="GtkImage" id="image725">
1278                                   <property name="visible">True</property>
1279                                   <property name="stock">gtk-zoom-in</property>
1280                                   <property name="icon_size">1</property>
1281                                   <property name="xalign">0.5</property>
1282                                   <property name="yalign">0.5</property>
1283                                   <property name="xpad">0</property>
1284                                   <property name="ypad">0</property>
1285                                 </widget>
1286                               </child>
1287                             </widget>
1288                           </child>
1289
1290                           <child>
1291                             <widget class="GtkImageMenuItem" id="decreaseFontSizeMenuItem">
1292                               <property name="visible">True</property>
1293                               <property name="label" translatable="yes">Zoom _Out</property>
1294                               <property name="use_underline">True</property>
1295                               <signal name="activate" handler="on_decreaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1296                               <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1297
1298                               <child internal-child="image">
1299                                 <widget class="GtkImage" id="image726">
1300                                   <property name="visible">True</property>
1301                                   <property name="stock">gtk-zoom-out</property>
1302                                   <property name="icon_size">1</property>
1303                                   <property name="xalign">0.5</property>
1304                                   <property name="yalign">0.5</property>
1305                                   <property name="xpad">0</property>
1306                                   <property name="ypad">0</property>
1307                                 </widget>
1308                               </child>
1309                             </widget>
1310                           </child>
1311
1312                           <child>
1313                             <widget class="GtkImageMenuItem" id="normalFontSizeMenuItem">
1314                               <property name="visible">True</property>
1315                               <property name="label" translatable="yes">_Normal Size</property>
1316                               <property name="use_underline">True</property>
1317                               <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1318
1319                               <child internal-child="image">
1320                                 <widget class="GtkImage" id="image727">
1321                                   <property name="visible">True</property>
1322                                   <property name="stock">gtk-zoom-100</property>
1323                                   <property name="icon_size">1</property>
1324                                   <property name="xalign">0.5</property>
1325                                   <property name="yalign">0.5</property>
1326                                   <property name="xpad">0</property>
1327                                   <property name="ypad">0</property>
1328                                 </widget>
1329                               </child>
1330                             </widget>
1331                           </child>
1332                         </widget>
1333                       </child>
1334                     </widget>
1335                   </child>
1336
1337                   <child>
1338                     <widget class="GtkMenuItem" id="debugMenu">
1339                       <property name="visible">True</property>
1340                       <property name="label" translatable="yes">_Debug</property>
1341                       <property name="use_underline">True</property>
1342
1343                       <child>
1344                         <widget class="GtkMenu" id="debugMenu_menu">
1345
1346                           <child>
1347                             <widget class="GtkSeparatorMenuItem" id="separator6">
1348                               <property name="visible">True</property>
1349                             </widget>
1350                           </child>
1351                         </widget>
1352                       </child>
1353                     </widget>
1354                   </child>
1355
1356                   <child>
1357                     <widget class="GtkMenuItem" id="helpMenu">
1358                       <property name="visible">True</property>
1359                       <property name="label" translatable="yes">_Help</property>
1360                       <property name="use_underline">True</property>
1361
1362                       <child>
1363                         <widget class="GtkMenu" id="helpMenu_menu">
1364
1365                           <child>
1366                             <widget class="GtkImageMenuItem" id="aboutMenuItem">
1367                               <property name="visible">True</property>
1368                               <property name="label" translatable="yes">_About</property>
1369                               <property name="use_underline">True</property>
1370
1371                               <child internal-child="image">
1372                                 <widget class="GtkImage" id="image728">
1373                                   <property name="visible">True</property>
1374                                   <property name="stock">gtk-about</property>
1375                                   <property name="icon_size">1</property>
1376                                   <property name="xalign">0.5</property>
1377                                   <property name="yalign">0.5</property>
1378                                   <property name="xpad">0</property>
1379                                   <property name="ypad">0</property>
1380                                 </widget>
1381                               </child>
1382                             </widget>
1383                           </child>
1384                         </widget>
1385                       </child>
1386                     </widget>
1387                   </child>
1388                 </widget>
1389               </child>
1390             </widget>
1391             <packing>
1392               <property name="padding">0</property>
1393               <property name="expand">False</property>
1394               <property name="fill">False</property>
1395             </packing>
1396           </child>
1397
1398           <child>
1399             <widget class="GtkHBox" id="hbox9">
1400               <property name="visible">True</property>
1401               <property name="homogeneous">False</property>
1402               <property name="spacing">0</property>
1403
1404               <child>
1405                 <widget class="GtkHPaned" id="hpaneScriptSequent">
1406                   <property name="visible">True</property>
1407                   <property name="can_focus">True</property>
1408
1409                   <child>
1410                     <widget class="GtkHBox" id="hbox18">
1411                       <property name="visible">True</property>
1412                       <property name="homogeneous">False</property>
1413                       <property name="spacing">0</property>
1414
1415                       <child>
1416                         <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1417                           <property name="visible">True</property>
1418                           <property name="shadow_type">GTK_SHADOW_OUT</property>
1419                           <property name="handle_position">GTK_POS_TOP</property>
1420                           <property name="snap_edge">GTK_POS_TOP</property>
1421
1422                           <child>
1423                             <widget class="GtkTable" id="ToolBarTable">
1424                               <property name="visible">True</property>
1425                               <property name="n_rows">17</property>
1426                               <property name="n_columns">2</property>
1427                               <property name="homogeneous">False</property>
1428                               <property name="row_spacing">4</property>
1429                               <property name="column_spacing">0</property>
1430
1431                               <child>
1432                                 <widget class="GtkButton" id="applyButton">
1433                                   <property name="visible">True</property>
1434                                   <property name="tooltip" translatable="yes">Apply</property>
1435                                   <property name="can_focus">True</property>
1436                                   <property name="label" translatable="yes">apply</property>
1437                                   <property name="use_underline">True</property>
1438                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1439                                   <property name="focus_on_click">True</property>
1440                                 </widget>
1441                                 <packing>
1442                                   <property name="left_attach">1</property>
1443                                   <property name="right_attach">2</property>
1444                                   <property name="top_attach">0</property>
1445                                   <property name="bottom_attach">1</property>
1446                                   <property name="x_options">fill</property>
1447                                   <property name="y_options"></property>
1448                                 </packing>
1449                               </child>
1450
1451                               <child>
1452                                 <widget class="GtkButton" id="introsButton">
1453                                   <property name="visible">True</property>
1454                                   <property name="tooltip" translatable="yes">Intros</property>
1455                                   <property name="can_focus">True</property>
1456                                   <property name="label" translatable="yes">intro</property>
1457                                   <property name="use_underline">True</property>
1458                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1459                                   <property name="focus_on_click">True</property>
1460                                 </widget>
1461                                 <packing>
1462                                   <property name="left_attach">0</property>
1463                                   <property name="right_attach">1</property>
1464                                   <property name="top_attach">0</property>
1465                                   <property name="bottom_attach">1</property>
1466                                   <property name="x_options">fill</property>
1467                                   <property name="y_options"></property>
1468                                 </packing>
1469                               </child>
1470
1471                               <child>
1472                                 <widget class="GtkButton" id="exactButton">
1473                                   <property name="visible">True</property>
1474                                   <property name="tooltip" translatable="yes">Exact</property>
1475                                   <property name="can_focus">True</property>
1476                                   <property name="label" translatable="yes">exact</property>
1477                                   <property name="use_underline">True</property>
1478                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1479                                   <property name="focus_on_click">True</property>
1480                                 </widget>
1481                                 <packing>
1482                                   <property name="left_attach">0</property>
1483                                   <property name="right_attach">1</property>
1484                                   <property name="top_attach">2</property>
1485                                   <property name="bottom_attach">3</property>
1486                                   <property name="x_options">fill</property>
1487                                   <property name="y_options"></property>
1488                                 </packing>
1489                               </child>
1490
1491                               <child>
1492                                 <widget class="GtkButton" id="elimButton">
1493                                   <property name="visible">True</property>
1494                                   <property name="tooltip" translatable="yes">Elim</property>
1495                                   <property name="can_focus">True</property>
1496                                   <property name="label" translatable="yes">elim</property>
1497                                   <property name="use_underline">True</property>
1498                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1499                                   <property name="focus_on_click">True</property>
1500                                 </widget>
1501                                 <packing>
1502                                   <property name="left_attach">0</property>
1503                                   <property name="right_attach">1</property>
1504                                   <property name="top_attach">4</property>
1505                                   <property name="bottom_attach">5</property>
1506                                   <property name="x_options">fill</property>
1507                                   <property name="y_options"></property>
1508                                 </packing>
1509                               </child>
1510
1511                               <child>
1512                                 <widget class="GtkButton" id="reflexivityButton">
1513                                   <property name="visible">True</property>
1514                                   <property name="tooltip" translatable="yes">Reflexivity</property>
1515                                   <property name="can_focus">True</property>
1516                                   <property name="label" translatable="yes">refl</property>
1517                                   <property name="use_underline">True</property>
1518                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1519                                   <property name="focus_on_click">True</property>
1520                                 </widget>
1521                                 <packing>
1522                                   <property name="left_attach">0</property>
1523                                   <property name="right_attach">1</property>
1524                                   <property name="top_attach">8</property>
1525                                   <property name="bottom_attach">9</property>
1526                                   <property name="x_options">fill</property>
1527                                   <property name="y_options"></property>
1528                                 </packing>
1529                               </child>
1530
1531                               <child>
1532                                 <widget class="GtkButton" id="symmetryButton">
1533                                   <property name="visible">True</property>
1534                                   <property name="tooltip" translatable="yes">Symmetry</property>
1535                                   <property name="can_focus">True</property>
1536                                   <property name="label" translatable="yes">sym</property>
1537                                   <property name="use_underline">True</property>
1538                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1539                                   <property name="focus_on_click">True</property>
1540                                 </widget>
1541                                 <packing>
1542                                   <property name="left_attach">1</property>
1543                                   <property name="right_attach">2</property>
1544                                   <property name="top_attach">8</property>
1545                                   <property name="bottom_attach">9</property>
1546                                   <property name="x_options">fill</property>
1547                                   <property name="y_options"></property>
1548                                 </packing>
1549                               </child>
1550
1551                               <child>
1552                                 <widget class="GtkButton" id="transitivityButton">
1553                                   <property name="visible">True</property>
1554                                   <property name="tooltip" translatable="yes">Transitivity</property>
1555                                   <property name="can_focus">True</property>
1556                                   <property name="label" translatable="yes">trans</property>
1557                                   <property name="use_underline">True</property>
1558                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1559                                   <property name="focus_on_click">True</property>
1560                                 </widget>
1561                                 <packing>
1562                                   <property name="left_attach">0</property>
1563                                   <property name="right_attach">1</property>
1564                                   <property name="top_attach">9</property>
1565                                   <property name="bottom_attach">10</property>
1566                                   <property name="x_options">fill</property>
1567                                   <property name="y_options"></property>
1568                                 </packing>
1569                               </child>
1570
1571                               <child>
1572                                 <widget class="GtkButton" id="simplifyButton">
1573                                   <property name="visible">True</property>
1574                                   <property name="tooltip" translatable="yes">Simplify</property>
1575                                   <property name="can_focus">True</property>
1576                                   <property name="label" translatable="yes">simpl</property>
1577                                   <property name="use_underline">True</property>
1578                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1579                                   <property name="focus_on_click">True</property>
1580                                 </widget>
1581                                 <packing>
1582                                   <property name="left_attach">0</property>
1583                                   <property name="right_attach">1</property>
1584                                   <property name="top_attach">11</property>
1585                                   <property name="bottom_attach">12</property>
1586                                   <property name="x_options">fill</property>
1587                                   <property name="y_options"></property>
1588                                 </packing>
1589                               </child>
1590
1591                               <child>
1592                                 <widget class="GtkButton" id="reduceButton">
1593                                   <property name="visible">True</property>
1594                                   <property name="tooltip" translatable="yes">Reduce</property>
1595                                   <property name="can_focus">True</property>
1596                                   <property name="label" translatable="yes">red</property>
1597                                   <property name="use_underline">True</property>
1598                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1599                                   <property name="focus_on_click">True</property>
1600                                 </widget>
1601                                 <packing>
1602                                   <property name="left_attach">1</property>
1603                                   <property name="right_attach">2</property>
1604                                   <property name="top_attach">11</property>
1605                                   <property name="bottom_attach">12</property>
1606                                   <property name="x_options">fill</property>
1607                                   <property name="y_options"></property>
1608                                 </packing>
1609                               </child>
1610
1611                               <child>
1612                                 <widget class="GtkButton" id="whdButton">
1613                                   <property name="visible">True</property>
1614                                   <property name="tooltip" translatable="yes">Whd</property>
1615                                   <property name="can_focus">True</property>
1616                                   <property name="label" translatable="yes">whd</property>
1617                                   <property name="use_underline">True</property>
1618                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1619                                   <property name="focus_on_click">True</property>
1620                                 </widget>
1621                                 <packing>
1622                                   <property name="left_attach">0</property>
1623                                   <property name="right_attach">1</property>
1624                                   <property name="top_attach">12</property>
1625                                   <property name="bottom_attach">13</property>
1626                                   <property name="x_options">fill</property>
1627                                   <property name="y_options"></property>
1628                                 </packing>
1629                               </child>
1630
1631                               <child>
1632                                 <widget class="GtkButton" id="assumptionButton">
1633                                   <property name="visible">True</property>
1634                                   <property name="tooltip" translatable="yes">Assumption</property>
1635                                   <property name="can_focus">True</property>
1636                                   <property name="label" translatable="yes">assum</property>
1637                                   <property name="use_underline">True</property>
1638                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1639                                   <property name="focus_on_click">True</property>
1640                                 </widget>
1641                                 <packing>
1642                                   <property name="left_attach">0</property>
1643                                   <property name="right_attach">1</property>
1644                                   <property name="top_attach">14</property>
1645                                   <property name="bottom_attach">15</property>
1646                                   <property name="x_options">fill</property>
1647                                   <property name="y_options"></property>
1648                                 </packing>
1649                               </child>
1650
1651                               <child>
1652                                 <widget class="GtkButton" id="autoButton">
1653                                   <property name="visible">True</property>
1654                                   <property name="tooltip" translatable="yes">Auto</property>
1655                                   <property name="can_focus">True</property>
1656                                   <property name="label" translatable="yes">auto</property>
1657                                   <property name="use_underline">True</property>
1658                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1659                                   <property name="focus_on_click">True</property>
1660                                 </widget>
1661                                 <packing>
1662                                   <property name="left_attach">1</property>
1663                                   <property name="right_attach">2</property>
1664                                   <property name="top_attach">14</property>
1665                                   <property name="bottom_attach">15</property>
1666                                   <property name="x_options">fill</property>
1667                                   <property name="y_options"></property>
1668                                 </packing>
1669                               </child>
1670
1671                               <child>
1672                                 <widget class="GtkButton" id="cutButton">
1673                                   <property name="visible">True</property>
1674                                   <property name="tooltip" translatable="yes">Cut</property>
1675                                   <property name="can_focus">True</property>
1676                                   <property name="label" translatable="yes">cut</property>
1677                                   <property name="use_underline">True</property>
1678                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1679                                   <property name="focus_on_click">True</property>
1680                                 </widget>
1681                                 <packing>
1682                                   <property name="left_attach">0</property>
1683                                   <property name="right_attach">1</property>
1684                                   <property name="top_attach">16</property>
1685                                   <property name="bottom_attach">17</property>
1686                                   <property name="x_options">fill</property>
1687                                   <property name="y_options"></property>
1688                                 </packing>
1689                               </child>
1690
1691                               <child>
1692                                 <widget class="GtkButton" id="replaceButton">
1693                                   <property name="visible">True</property>
1694                                   <property name="tooltip" translatable="yes">Replace</property>
1695                                   <property name="can_focus">True</property>
1696                                   <property name="label" translatable="yes">repl</property>
1697                                   <property name="use_underline">True</property>
1698                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1699                                   <property name="focus_on_click">True</property>
1700                                 </widget>
1701                                 <packing>
1702                                   <property name="left_attach">1</property>
1703                                   <property name="right_attach">2</property>
1704                                   <property name="top_attach">16</property>
1705                                   <property name="bottom_attach">17</property>
1706                                   <property name="x_options">fill</property>
1707                                   <property name="y_options"></property>
1708                                 </packing>
1709                               </child>
1710
1711                               <child>
1712                                 <widget class="GtkButton" id="elimTypeButton">
1713                                   <property name="visible">True</property>
1714                                   <property name="tooltip" translatable="yes">ElimType</property>
1715                                   <property name="can_focus">True</property>
1716                                   <property name="label" translatable="yes">elimTy</property>
1717                                   <property name="use_underline">True</property>
1718                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1719                                   <property name="focus_on_click">True</property>
1720                                 </widget>
1721                                 <packing>
1722                                   <property name="left_attach">1</property>
1723                                   <property name="right_attach">2</property>
1724                                   <property name="top_attach">4</property>
1725                                   <property name="bottom_attach">5</property>
1726                                   <property name="x_options">fill</property>
1727                                   <property name="y_options"></property>
1728                                 </packing>
1729                               </child>
1730
1731                               <child>
1732                                 <widget class="GtkHBox" id="hbox18">
1733                                   <property name="visible">True</property>
1734                                   <property name="homogeneous">True</property>
1735                                   <property name="spacing">0</property>
1736
1737                                   <child>
1738                                     <widget class="GtkButton" id="rightButton">
1739                                       <property name="visible">True</property>
1740                                       <property name="tooltip" translatable="yes">Right</property>
1741                                       <property name="can_focus">True</property>
1742                                       <property name="label" translatable="yes">R</property>
1743                                       <property name="use_underline">True</property>
1744                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1745                                       <property name="focus_on_click">True</property>
1746                                     </widget>
1747                                     <packing>
1748                                       <property name="padding">0</property>
1749                                       <property name="expand">True</property>
1750                                       <property name="fill">True</property>
1751                                     </packing>
1752                                   </child>
1753
1754                                   <child>
1755                                     <widget class="GtkButton" id="existsButton">
1756                                       <property name="visible">True</property>
1757                                       <property name="tooltip" translatable="yes">Exists</property>
1758                                       <property name="can_focus">True</property>
1759                                       <property name="label" translatable="yes">∃</property>
1760                                       <property name="use_underline">True</property>
1761                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1762                                       <property name="focus_on_click">True</property>
1763                                     </widget>
1764                                     <packing>
1765                                       <property name="padding">0</property>
1766                                       <property name="expand">True</property>
1767                                       <property name="fill">True</property>
1768                                     </packing>
1769                                   </child>
1770                                 </widget>
1771                                 <packing>
1772                                   <property name="left_attach">1</property>
1773                                   <property name="right_attach">2</property>
1774                                   <property name="top_attach">6</property>
1775                                   <property name="bottom_attach">7</property>
1776                                   <property name="x_options">fill</property>
1777                                   <property name="y_options">fill</property>
1778                                 </packing>
1779                               </child>
1780
1781                               <child>
1782                                 <widget class="GtkHBox" id="hbox17">
1783                                   <property name="visible">True</property>
1784                                   <property name="homogeneous">True</property>
1785                                   <property name="spacing">0</property>
1786
1787                                   <child>
1788                                     <widget class="GtkButton" id="splitButton">
1789                                       <property name="visible">True</property>
1790                                       <property name="tooltip" translatable="yes">Split</property>
1791                                       <property name="can_focus">True</property>
1792                                       <property name="label" translatable="yes">∧</property>
1793                                       <property name="use_underline">True</property>
1794                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1795                                       <property name="focus_on_click">True</property>
1796                                     </widget>
1797                                     <packing>
1798                                       <property name="padding">0</property>
1799                                       <property name="expand">True</property>
1800                                       <property name="fill">True</property>
1801                                     </packing>
1802                                   </child>
1803
1804                                   <child>
1805                                     <widget class="GtkButton" id="leftButton">
1806                                       <property name="visible">True</property>
1807                                       <property name="tooltip" translatable="yes">Left</property>
1808                                       <property name="can_focus">True</property>
1809                                       <property name="label" translatable="yes">L</property>
1810                                       <property name="use_underline">True</property>
1811                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1812                                       <property name="focus_on_click">True</property>
1813                                     </widget>
1814                                     <packing>
1815                                       <property name="padding">0</property>
1816                                       <property name="expand">True</property>
1817                                       <property name="fill">True</property>
1818                                     </packing>
1819                                   </child>
1820                                 </widget>
1821                                 <packing>
1822                                   <property name="left_attach">0</property>
1823                                   <property name="right_attach">1</property>
1824                                   <property name="top_attach">6</property>
1825                                   <property name="bottom_attach">7</property>
1826                                   <property name="x_options">fill</property>
1827                                   <property name="y_options">fill</property>
1828                                 </packing>
1829                               </child>
1830
1831                               <child>
1832                                 <widget class="GtkAlignment" id="alignment6">
1833                                   <property name="visible">True</property>
1834                                   <property name="xalign">0.5</property>
1835                                   <property name="yalign">0.5</property>
1836                                   <property name="xscale">1</property>
1837                                   <property name="yscale">1</property>
1838                                   <property name="top_padding">0</property>
1839                                   <property name="bottom_padding">0</property>
1840                                   <property name="left_padding">0</property>
1841                                   <property name="right_padding">0</property>
1842
1843                                   <child>
1844                                     <placeholder/>
1845                                   </child>
1846                                 </widget>
1847                                 <packing>
1848                                   <property name="left_attach">0</property>
1849                                   <property name="right_attach">1</property>
1850                                   <property name="top_attach">1</property>
1851                                   <property name="bottom_attach">2</property>
1852                                   <property name="x_options">fill</property>
1853                                 </packing>
1854                               </child>
1855
1856                               <child>
1857                                 <widget class="GtkAlignment" id="alignment7">
1858                                   <property name="visible">True</property>
1859                                   <property name="xalign">0.5</property>
1860                                   <property name="yalign">0.5</property>
1861                                   <property name="xscale">1</property>
1862                                   <property name="yscale">1</property>
1863                                   <property name="top_padding">0</property>
1864                                   <property name="bottom_padding">0</property>
1865                                   <property name="left_padding">0</property>
1866                                   <property name="right_padding">0</property>
1867
1868                                   <child>
1869                                     <placeholder/>
1870                                   </child>
1871                                 </widget>
1872                                 <packing>
1873                                   <property name="left_attach">0</property>
1874                                   <property name="right_attach">1</property>
1875                                   <property name="top_attach">3</property>
1876                                   <property name="bottom_attach">4</property>
1877                                   <property name="x_options">fill</property>
1878                                 </packing>
1879                               </child>
1880
1881                               <child>
1882                                 <widget class="GtkAlignment" id="alignment8">
1883                                   <property name="visible">True</property>
1884                                   <property name="xalign">0.5</property>
1885                                   <property name="yalign">0.5</property>
1886                                   <property name="xscale">1</property>
1887                                   <property name="yscale">1</property>
1888                                   <property name="top_padding">0</property>
1889                                   <property name="bottom_padding">0</property>
1890                                   <property name="left_padding">0</property>
1891                                   <property name="right_padding">0</property>
1892
1893                                   <child>
1894                                     <placeholder/>
1895                                   </child>
1896                                 </widget>
1897                                 <packing>
1898                                   <property name="left_attach">0</property>
1899                                   <property name="right_attach">1</property>
1900                                   <property name="top_attach">5</property>
1901                                   <property name="bottom_attach">6</property>
1902                                   <property name="x_options">fill</property>
1903                                 </packing>
1904                               </child>
1905
1906                               <child>
1907                                 <widget class="GtkAlignment" id="alignment9">
1908                                   <property name="visible">True</property>
1909                                   <property name="xalign">0.5</property>
1910                                   <property name="yalign">0.5</property>
1911                                   <property name="xscale">1</property>
1912                                   <property name="yscale">1</property>
1913                                   <property name="top_padding">0</property>
1914                                   <property name="bottom_padding">0</property>
1915                                   <property name="left_padding">0</property>
1916                                   <property name="right_padding">0</property>
1917
1918                                   <child>
1919                                     <placeholder/>
1920                                   </child>
1921                                 </widget>
1922                                 <packing>
1923                                   <property name="left_attach">0</property>
1924                                   <property name="right_attach">1</property>
1925                                   <property name="top_attach">7</property>
1926                                   <property name="bottom_attach">8</property>
1927                                   <property name="x_options">fill</property>
1928                                 </packing>
1929                               </child>
1930
1931                               <child>
1932                                 <widget class="GtkAlignment" id="alignment10">
1933                                   <property name="visible">True</property>
1934                                   <property name="xalign">0.5</property>
1935                                   <property name="yalign">0.5</property>
1936                                   <property name="xscale">1</property>
1937                                   <property name="yscale">1</property>
1938                                   <property name="top_padding">0</property>
1939                                   <property name="bottom_padding">0</property>
1940                                   <property name="left_padding">0</property>
1941                                   <property name="right_padding">0</property>
1942
1943                                   <child>
1944                                     <placeholder/>
1945                                   </child>
1946                                 </widget>
1947                                 <packing>
1948                                   <property name="left_attach">0</property>
1949                                   <property name="right_attach">1</property>
1950                                   <property name="top_attach">10</property>
1951                                   <property name="bottom_attach">11</property>
1952                                   <property name="x_options">fill</property>
1953                                 </packing>
1954                               </child>
1955
1956                               <child>
1957                                 <widget class="GtkAlignment" id="alignment11">
1958                                   <property name="visible">True</property>
1959                                   <property name="xalign">0.5</property>
1960                                   <property name="yalign">0.5</property>
1961                                   <property name="xscale">1</property>
1962                                   <property name="yscale">1</property>
1963                                   <property name="top_padding">0</property>
1964                                   <property name="bottom_padding">0</property>
1965                                   <property name="left_padding">0</property>
1966                                   <property name="right_padding">0</property>
1967
1968                                   <child>
1969                                     <placeholder/>
1970                                   </child>
1971                                 </widget>
1972                                 <packing>
1973                                   <property name="left_attach">0</property>
1974                                   <property name="right_attach">1</property>
1975                                   <property name="top_attach">13</property>
1976                                   <property name="bottom_attach">14</property>
1977                                   <property name="x_options">fill</property>
1978                                 </packing>
1979                               </child>
1980
1981                               <child>
1982                                 <widget class="GtkAlignment" id="alignment12">
1983                                   <property name="visible">True</property>
1984                                   <property name="xalign">0.5</property>
1985                                   <property name="yalign">0.5</property>
1986                                   <property name="xscale">1</property>
1987                                   <property name="yscale">1</property>
1988                                   <property name="top_padding">0</property>
1989                                   <property name="bottom_padding">0</property>
1990                                   <property name="left_padding">0</property>
1991                                   <property name="right_padding">0</property>
1992
1993                                   <child>
1994                                     <placeholder/>
1995                                   </child>
1996                                 </widget>
1997                                 <packing>
1998                                   <property name="left_attach">0</property>
1999                                   <property name="right_attach">1</property>
2000                                   <property name="top_attach">15</property>
2001                                   <property name="bottom_attach">16</property>
2002                                   <property name="x_options">fill</property>
2003                                 </packing>
2004                               </child>
2005                             </widget>
2006                           </child>
2007                         </widget>
2008                         <packing>
2009                           <property name="padding">0</property>
2010                           <property name="expand">False</property>
2011                           <property name="fill">True</property>
2012                         </packing>
2013                       </child>
2014
2015                       <child>
2016                         <widget class="GtkVBox" id="vboxScript">
2017                           <property name="width_request">400</property>
2018                           <property name="visible">True</property>
2019                           <property name="homogeneous">False</property>
2020                           <property name="spacing">0</property>
2021
2022                           <child>
2023                             <widget class="GtkToolbar" id="buttonsToolbar">
2024                               <property name="visible">True</property>
2025                               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
2026                               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
2027                               <property name="tooltips">True</property>
2028                               <property name="show_arrow">True</property>
2029
2030                               <child>
2031                                 <widget class="GtkToolItem" id="toolitem25">
2032                                   <property name="visible">True</property>
2033                                   <property name="visible_horizontal">True</property>
2034                                   <property name="visible_vertical">True</property>
2035                                   <property name="is_important">False</property>
2036
2037                                   <child>
2038                                     <widget class="GtkButton" id="scriptTopButton">
2039                                       <property name="visible">True</property>
2040                                       <property name="tooltip" translatable="yes">restart (Ctrl+Home)</property>
2041                                       <property name="can_focus">True</property>
2042                                       <property name="relief">GTK_RELIEF_NONE</property>
2043                                       <property name="focus_on_click">True</property>
2044                                       <accelerator key="Home" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
2045
2046                                       <child>
2047                                         <widget class="GtkImage" id="image253">
2048                                           <property name="visible">True</property>
2049                                           <property name="stock">gtk-goto-top</property>
2050                                           <property name="icon_size">4</property>
2051                                           <property name="xalign">0.5</property>
2052                                           <property name="yalign">0.5</property>
2053                                           <property name="xpad">0</property>
2054                                           <property name="ypad">0</property>
2055                                         </widget>
2056                                       </child>
2057                                     </widget>
2058                                   </child>
2059                                 </widget>
2060                                 <packing>
2061                                   <property name="expand">False</property>
2062                                   <property name="homogeneous">False</property>
2063                                 </packing>
2064                               </child>
2065
2066                               <child>
2067                                 <widget class="GtkToolItem" id="toolitem26">
2068                                   <property name="visible">True</property>
2069                                   <property name="visible_horizontal">True</property>
2070                                   <property name="visible_vertical">True</property>
2071                                   <property name="is_important">False</property>
2072
2073                                   <child>
2074                                     <widget class="GtkButton" id="scriptRetractButton">
2075                                       <property name="visible">True</property>
2076                                       <property name="tooltip" translatable="yes">go back 1 phrase (Ctrl+Page Up)</property>
2077                                       <property name="can_focus">True</property>
2078                                       <property name="relief">GTK_RELIEF_NONE</property>
2079                                       <property name="focus_on_click">True</property>
2080                                       <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
2081
2082                                       <child>
2083                                         <widget class="GtkImage" id="image254">
2084                                           <property name="visible">True</property>
2085                                           <property name="stock">gtk-go-up</property>
2086                                           <property name="icon_size">4</property>
2087                                           <property name="xalign">0.5</property>
2088                                           <property name="yalign">0.5</property>
2089                                           <property name="xpad">0</property>
2090                                           <property name="ypad">0</property>
2091                                         </widget>
2092                                       </child>
2093                                     </widget>
2094                                   </child>
2095                                 </widget>
2096                                 <packing>
2097                                   <property name="expand">False</property>
2098                                   <property name="homogeneous">False</property>
2099                                 </packing>
2100                               </child>
2101
2102                               <child>
2103                                 <widget class="GtkToolItem" id="toolitem27">
2104                                   <property name="visible">True</property>
2105                                   <property name="visible_horizontal">True</property>
2106                                   <property name="visible_vertical">True</property>
2107                                   <property name="is_important">False</property>
2108
2109                                   <child>
2110                                     <widget class="GtkButton" id="scriptJumpButton">
2111                                       <property name="visible">True</property>
2112                                       <property name="tooltip" translatable="yes">execute until point</property>
2113                                       <property name="can_focus">True</property>
2114                                       <property name="relief">GTK_RELIEF_NONE</property>
2115                                       <property name="focus_on_click">True</property>
2116
2117                                       <child>
2118                                         <widget class="GtkImage" id="image255">
2119                                           <property name="visible">True</property>
2120                                           <property name="stock">gtk-jump-to</property>
2121                                           <property name="icon_size">4</property>
2122                                           <property name="xalign">0.5</property>
2123                                           <property name="yalign">0.5</property>
2124                                           <property name="xpad">0</property>
2125                                           <property name="ypad">0</property>
2126                                         </widget>
2127                                       </child>
2128                                     </widget>
2129                                   </child>
2130                                 </widget>
2131                                 <packing>
2132                                   <property name="expand">False</property>
2133                                   <property name="homogeneous">False</property>
2134                                 </packing>
2135                               </child>
2136
2137                               <child>
2138                                 <widget class="GtkToolItem" id="toolitem28">
2139                                   <property name="visible">True</property>
2140                                   <property name="visible_horizontal">True</property>
2141                                   <property name="visible_vertical">True</property>
2142                                   <property name="is_important">False</property>
2143
2144                                   <child>
2145                                     <widget class="GtkButton" id="scriptAdvanceButton">
2146                                       <property name="visible">True</property>
2147                                       <property name="tooltip" translatable="yes">go forward 1 phrase (Ctrl+Page Down)</property>
2148                                       <property name="can_focus">True</property>
2149                                       <property name="relief">GTK_RELIEF_NONE</property>
2150                                       <property name="focus_on_click">True</property>
2151                                       <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
2152
2153                                       <child>
2154                                         <widget class="GtkImage" id="image256">
2155                                           <property name="visible">True</property>
2156                                           <property name="stock">gtk-go-down</property>
2157                                           <property name="icon_size">4</property>
2158                                           <property name="xalign">0.5</property>
2159                                           <property name="yalign">0.5</property>
2160                                           <property name="xpad">0</property>
2161                                           <property name="ypad">0</property>
2162                                         </widget>
2163                                       </child>
2164                                     </widget>
2165                                   </child>
2166                                 </widget>
2167                                 <packing>
2168                                   <property name="expand">False</property>
2169                                   <property name="homogeneous">False</property>
2170                                 </packing>
2171                               </child>
2172
2173                               <child>
2174                                 <widget class="GtkToolItem" id="toolitem29">
2175                                   <property name="visible">True</property>
2176                                   <property name="visible_horizontal">True</property>
2177                                   <property name="visible_vertical">True</property>
2178                                   <property name="is_important">False</property>
2179
2180                                   <child>
2181                                     <widget class="GtkButton" id="scriptBottomButton">
2182                                       <property name="visible">True</property>
2183                                       <property name="tooltip" translatable="yes">execute all (Ctrl+End)</property>
2184                                       <property name="can_focus">True</property>
2185                                       <property name="relief">GTK_RELIEF_NONE</property>
2186                                       <property name="focus_on_click">True</property>
2187                                       <accelerator key="End" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
2188
2189                                       <child>
2190                                         <widget class="GtkImage" id="image257">
2191                                           <property name="visible">True</property>
2192                                           <property name="stock">gtk-goto-bottom</property>
2193                                           <property name="icon_size">4</property>
2194                                           <property name="xalign">0.5</property>
2195                                           <property name="yalign">0.5</property>
2196                                           <property name="xpad">0</property>
2197                                           <property name="ypad">0</property>
2198                                         </widget>
2199                                       </child>
2200                                     </widget>
2201                                   </child>
2202                                 </widget>
2203                                 <packing>
2204                                   <property name="expand">False</property>
2205                                   <property name="homogeneous">False</property>
2206                                 </packing>
2207                               </child>
2208                             </widget>
2209                             <packing>
2210                               <property name="padding">0</property>
2211                               <property name="expand">False</property>
2212                               <property name="fill">False</property>
2213                             </packing>
2214                           </child>
2215
2216                           <child>
2217                             <widget class="GtkNotebook" id="scriptNotebook">
2218                               <property name="visible">True</property>
2219                               <property name="can_focus">True</property>
2220                               <property name="show_tabs">True</property>
2221                               <property name="show_border">True</property>
2222                               <property name="tab_pos">GTK_POS_BOTTOM</property>
2223                               <property name="scrollable">False</property>
2224                               <property name="enable_popup">False</property>
2225
2226                               <child>
2227                                 <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
2228                                   <property name="visible">True</property>
2229                                   <property name="can_focus">True</property>
2230                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2231                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2232                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2233                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2234
2235                                   <child>
2236                                     <placeholder/>
2237                                   </child>
2238                                 </widget>
2239                                 <packing>
2240                                   <property name="tab_expand">False</property>
2241                                   <property name="tab_fill">True</property>
2242                                 </packing>
2243                               </child>
2244
2245                               <child>
2246                                 <widget class="GtkLabel" id="scriptLabel">
2247                                   <property name="visible">True</property>
2248                                   <property name="label" translatable="yes">script</property>
2249                                   <property name="use_underline">False</property>
2250                                   <property name="use_markup">False</property>
2251                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2252                                   <property name="wrap">False</property>
2253                                   <property name="selectable">False</property>
2254                                   <property name="xalign">0.5</property>
2255                                   <property name="yalign">0.5</property>
2256                                   <property name="xpad">0</property>
2257                                   <property name="ypad">0</property>
2258                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2259                                   <property name="width_chars">-1</property>
2260                                   <property name="single_line_mode">False</property>
2261                                   <property name="angle">0</property>
2262                                 </widget>
2263                                 <packing>
2264                                   <property name="type">tab</property>
2265                                 </packing>
2266                               </child>
2267
2268                               <child>
2269                                 <widget class="GtkScrolledWindow" id="scrolledwindow8">
2270                                   <property name="visible">True</property>
2271                                   <property name="can_focus">True</property>
2272                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2273                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2274                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
2275                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2276
2277                                   <child>
2278                                     <widget class="GtkTreeView" id="scriptTreeView">
2279                                       <property name="visible">True</property>
2280                                       <property name="can_focus">True</property>
2281                                       <property name="headers_visible">False</property>
2282                                       <property name="rules_hint">False</property>
2283                                       <property name="reorderable">False</property>
2284                                       <property name="enable_search">True</property>
2285                                       <property name="fixed_height_mode">False</property>
2286                                       <property name="hover_selection">False</property>
2287                                       <property name="hover_expand">False</property>
2288                                     </widget>
2289                                   </child>
2290                                 </widget>
2291                                 <packing>
2292                                   <property name="tab_expand">False</property>
2293                                   <property name="tab_fill">True</property>
2294                                 </packing>
2295                               </child>
2296
2297                               <child>
2298                                 <widget class="GtkLabel" id="label13">
2299                                   <property name="visible">True</property>
2300                                   <property name="label" translatable="yes">outline</property>
2301                                   <property name="use_underline">False</property>
2302                                   <property name="use_markup">False</property>
2303                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2304                                   <property name="wrap">False</property>
2305                                   <property name="selectable">False</property>
2306                                   <property name="xalign">0.5</property>
2307                                   <property name="yalign">0.5</property>
2308                                   <property name="xpad">0</property>
2309                                   <property name="ypad">0</property>
2310                                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2311                                   <property name="width_chars">-1</property>
2312                                   <property name="single_line_mode">False</property>
2313                                   <property name="angle">0</property>
2314                                 </widget>
2315                                 <packing>
2316                                   <property name="type">tab</property>
2317                                 </packing>
2318                               </child>
2319                             </widget>
2320                             <packing>
2321                               <property name="padding">0</property>
2322                               <property name="expand">True</property>
2323                               <property name="fill">True</property>
2324                             </packing>
2325                           </child>
2326                         </widget>
2327                         <packing>
2328                           <property name="padding">0</property>
2329                           <property name="expand">True</property>
2330                           <property name="fill">True</property>
2331                         </packing>
2332                       </child>
2333                     </widget>
2334                     <packing>
2335                       <property name="shrink">True</property>
2336                       <property name="resize">False</property>
2337                     </packing>
2338                   </child>
2339
2340                   <child>
2341                     <widget class="GtkVPaned" id="vpaned1">
2342                       <property name="width_request">250</property>
2343                       <property name="height_request">500</property>
2344                       <property name="visible">True</property>
2345                       <property name="can_focus">True</property>
2346                       <property name="position">380</property>
2347
2348                       <child>
2349                         <widget class="GtkNotebook" id="sequentsNotebook">
2350                           <property name="visible">True</property>
2351                           <property name="can_focus">True</property>
2352                           <property name="show_tabs">True</property>
2353                           <property name="show_border">True</property>
2354                           <property name="tab_pos">GTK_POS_TOP</property>
2355                           <property name="scrollable">False</property>
2356                           <property name="enable_popup">False</property>
2357                         </widget>
2358                         <packing>
2359                           <property name="shrink">True</property>
2360                           <property name="resize">False</property>
2361                         </packing>
2362                       </child>
2363
2364                       <child>
2365                         <widget class="GtkHBox" id="hbox9">
2366                           <property name="visible">True</property>
2367                           <property name="homogeneous">False</property>
2368                           <property name="spacing">0</property>
2369
2370                           <child>
2371                             <widget class="GtkScrolledWindow" id="logScrolledWin">
2372                               <property name="visible">True</property>
2373                               <property name="can_focus">True</property>
2374                               <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
2375                               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2376                               <property name="shadow_type">GTK_SHADOW_IN</property>
2377                               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2378
2379                               <child>
2380                                 <widget class="GtkTextView" id="logTextView">
2381                                   <property name="visible">True</property>
2382                                   <property name="can_focus">True</property>
2383                                   <property name="editable">False</property>
2384                                   <property name="overwrite">False</property>
2385                                   <property name="accepts_tab">True</property>
2386                                   <property name="justification">GTK_JUSTIFY_LEFT</property>
2387                                   <property name="wrap_mode">GTK_WRAP_CHAR</property>
2388                                   <property name="cursor_visible">False</property>
2389                                   <property name="pixels_above_lines">0</property>
2390                                   <property name="pixels_below_lines">0</property>
2391                                   <property name="pixels_inside_wrap">0</property>
2392                                   <property name="left_margin">0</property>
2393                                   <property name="right_margin">0</property>
2394                                   <property name="indent">0</property>
2395                                   <property name="text" translatable="yes"></property>
2396                                 </widget>
2397                               </child>
2398                             </widget>
2399                             <packing>
2400                               <property name="padding">0</property>
2401                               <property name="expand">True</property>
2402                               <property name="fill">True</property>
2403                             </packing>
2404                           </child>
2405                         </widget>
2406                         <packing>
2407                           <property name="shrink">True</property>
2408                           <property name="resize">True</property>
2409                         </packing>
2410                       </child>
2411                     </widget>
2412                     <packing>
2413                       <property name="shrink">True</property>
2414                       <property name="resize">True</property>
2415                     </packing>
2416                   </child>
2417                 </widget>
2418                 <packing>
2419                   <property name="padding">0</property>
2420                   <property name="expand">True</property>
2421                   <property name="fill">True</property>
2422                 </packing>
2423               </child>
2424             </widget>
2425             <packing>
2426               <property name="padding">0</property>
2427               <property name="expand">True</property>
2428               <property name="fill">True</property>
2429             </packing>
2430           </child>
2431
2432           <child>
2433             <widget class="GtkHBox" id="hbox10">
2434               <property name="visible">True</property>
2435               <property name="homogeneous">False</property>
2436               <property name="spacing">0</property>
2437
2438               <child>
2439                 <widget class="GtkStatusbar" id="StatusBar">
2440                   <property name="visible">True</property>
2441                   <property name="has_resize_grip">False</property>
2442                 </widget>
2443                 <packing>
2444                   <property name="padding">0</property>
2445                   <property name="expand">True</property>
2446                   <property name="fill">True</property>
2447                 </packing>
2448               </child>
2449
2450               <child>
2451                 <widget class="GtkNotebook" id="HintNotebook">
2452                   <property name="visible">True</property>
2453                   <property name="show_tabs">False</property>
2454                   <property name="show_border">True</property>
2455                   <property name="tab_pos">GTK_POS_TOP</property>
2456                   <property name="scrollable">False</property>
2457                   <property name="enable_popup">False</property>
2458
2459                   <child>
2460                     <widget class="GtkImage" id="HintLowImage">
2461                       <property name="visible">True</property>
2462                       <property name="xalign">0.5</property>
2463                       <property name="yalign">0.5</property>
2464                       <property name="xpad">0</property>
2465                       <property name="ypad">0</property>
2466                     </widget>
2467                     <packing>
2468                       <property name="tab_expand">False</property>
2469                       <property name="tab_fill">True</property>
2470                     </packing>
2471                   </child>
2472
2473                   <child>
2474                     <widget class="GtkLabel" id="label14">
2475                       <property name="visible">True</property>
2476                       <property name="label" translatable="yes">label14</property>
2477                       <property name="use_underline">False</property>
2478                       <property name="use_markup">False</property>
2479                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2480                       <property name="wrap">False</property>
2481                       <property name="selectable">False</property>
2482                       <property name="xalign">0.5</property>
2483                       <property name="yalign">0.5</property>
2484                       <property name="xpad">0</property>
2485                       <property name="ypad">0</property>
2486                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2487                       <property name="width_chars">-1</property>
2488                       <property name="single_line_mode">False</property>
2489                       <property name="angle">0</property>
2490                     </widget>
2491                     <packing>
2492                       <property name="type">tab</property>
2493                     </packing>
2494                   </child>
2495
2496                   <child>
2497                     <widget class="GtkImage" id="HintMediumImage">
2498                       <property name="visible">True</property>
2499                       <property name="xalign">0.5</property>
2500                       <property name="yalign">0.5</property>
2501                       <property name="xpad">0</property>
2502                       <property name="ypad">0</property>
2503                     </widget>
2504                     <packing>
2505                       <property name="tab_expand">False</property>
2506                       <property name="tab_fill">True</property>
2507                     </packing>
2508                   </child>
2509
2510                   <child>
2511                     <widget class="GtkLabel" id="label15">
2512                       <property name="visible">True</property>
2513                       <property name="label" translatable="yes">label15</property>
2514                       <property name="use_underline">False</property>
2515                       <property name="use_markup">False</property>
2516                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2517                       <property name="wrap">False</property>
2518                       <property name="selectable">False</property>
2519                       <property name="xalign">0.5</property>
2520                       <property name="yalign">0.5</property>
2521                       <property name="xpad">0</property>
2522                       <property name="ypad">0</property>
2523                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2524                       <property name="width_chars">-1</property>
2525                       <property name="single_line_mode">False</property>
2526                       <property name="angle">0</property>
2527                     </widget>
2528                     <packing>
2529                       <property name="type">tab</property>
2530                     </packing>
2531                   </child>
2532
2533                   <child>
2534                     <widget class="GtkImage" id="HintHighImage">
2535                       <property name="visible">True</property>
2536                       <property name="xalign">0.5</property>
2537                       <property name="yalign">0.5</property>
2538                       <property name="xpad">0</property>
2539                       <property name="ypad">0</property>
2540                     </widget>
2541                     <packing>
2542                       <property name="tab_expand">False</property>
2543                       <property name="tab_fill">True</property>
2544                     </packing>
2545                   </child>
2546
2547                   <child>
2548                     <widget class="GtkLabel" id="label16">
2549                       <property name="visible">True</property>
2550                       <property name="label" translatable="yes">label16</property>
2551                       <property name="use_underline">False</property>
2552                       <property name="use_markup">False</property>
2553                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2554                       <property name="wrap">False</property>
2555                       <property name="selectable">False</property>
2556                       <property name="xalign">0.5</property>
2557                       <property name="yalign">0.5</property>
2558                       <property name="xpad">0</property>
2559                       <property name="ypad">0</property>
2560                       <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2561                       <property name="width_chars">-1</property>
2562                       <property name="single_line_mode">False</property>
2563                       <property name="angle">0</property>
2564                     </widget>
2565                     <packing>
2566                       <property name="type">tab</property>
2567                     </packing>
2568                   </child>
2569                 </widget>
2570                 <packing>
2571                   <property name="padding">0</property>
2572                   <property name="expand">False</property>
2573                   <property name="fill">True</property>
2574                 </packing>
2575               </child>
2576             </widget>
2577             <packing>
2578               <property name="padding">0</property>
2579               <property name="expand">False</property>
2580               <property name="fill">False</property>
2581             </packing>
2582           </child>
2583         </widget>
2584       </child>
2585     </widget>
2586   </child>
2587 </widget>
2588
2589 <widget class="GtkDialog" id="TextDialog">
2590   <property name="title" translatable="yes">DUMMY</property>
2591   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2592   <property name="window_position">GTK_WIN_POS_NONE</property>
2593   <property name="modal">False</property>
2594   <property name="resizable">True</property>
2595   <property name="destroy_with_parent">False</property>
2596   <property name="decorated">True</property>
2597   <property name="skip_taskbar_hint">False</property>
2598   <property name="skip_pager_hint">False</property>
2599   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2600   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2601   <property name="focus_on_map">True</property>
2602   <property name="has_separator">True</property>
2603
2604   <child internal-child="vbox">
2605     <widget class="GtkVBox" id="vbox5">
2606       <property name="visible">True</property>
2607       <property name="homogeneous">False</property>
2608       <property name="spacing">0</property>
2609
2610       <child internal-child="action_area">
2611         <widget class="GtkHButtonBox" id="hbuttonbox1">
2612           <property name="visible">True</property>
2613           <property name="layout_style">GTK_BUTTONBOX_END</property>
2614
2615           <child>
2616             <widget class="GtkButton" id="TextDialogCancelButton">
2617               <property name="visible">True</property>
2618               <property name="can_default">True</property>
2619               <property name="can_focus">True</property>
2620               <property name="label">gtk-cancel</property>
2621               <property name="use_stock">True</property>
2622               <property name="relief">GTK_RELIEF_NORMAL</property>
2623               <property name="focus_on_click">True</property>
2624               <property name="response_id">-6</property>
2625             </widget>
2626           </child>
2627
2628           <child>
2629             <widget class="GtkButton" id="TextDialogOkButton">
2630               <property name="visible">True</property>
2631               <property name="can_default">True</property>
2632               <property name="can_focus">True</property>
2633               <property name="label">gtk-ok</property>
2634               <property name="use_stock">True</property>
2635               <property name="relief">GTK_RELIEF_NORMAL</property>
2636               <property name="focus_on_click">True</property>
2637               <property name="response_id">-5</property>
2638             </widget>
2639           </child>
2640         </widget>
2641         <packing>
2642           <property name="padding">0</property>
2643           <property name="expand">False</property>
2644           <property name="fill">True</property>
2645           <property name="pack_type">GTK_PACK_END</property>
2646         </packing>
2647       </child>
2648
2649       <child>
2650         <widget class="GtkLabel" id="TextDialogLabel">
2651           <property name="visible">True</property>
2652           <property name="label" translatable="yes">DUMMY</property>
2653           <property name="use_underline">False</property>
2654           <property name="use_markup">False</property>
2655           <property name="justify">GTK_JUSTIFY_LEFT</property>
2656           <property name="wrap">False</property>
2657           <property name="selectable">False</property>
2658           <property name="xalign">0.5</property>
2659           <property name="yalign">0.5</property>
2660           <property name="xpad">0</property>
2661           <property name="ypad">0</property>
2662           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2663           <property name="width_chars">-1</property>
2664           <property name="single_line_mode">False</property>
2665           <property name="angle">0</property>
2666         </widget>
2667         <packing>
2668           <property name="padding">0</property>
2669           <property name="expand">False</property>
2670           <property name="fill">False</property>
2671         </packing>
2672       </child>
2673
2674       <child>
2675         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2676           <property name="visible">True</property>
2677           <property name="can_focus">True</property>
2678           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2679           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2680           <property name="shadow_type">GTK_SHADOW_IN</property>
2681           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2682
2683           <child>
2684             <widget class="GtkTextView" id="TextDialogTextView">
2685               <property name="visible">True</property>
2686               <property name="can_focus">True</property>
2687               <property name="editable">True</property>
2688               <property name="overwrite">False</property>
2689               <property name="accepts_tab">True</property>
2690               <property name="justification">GTK_JUSTIFY_LEFT</property>
2691               <property name="wrap_mode">GTK_WRAP_NONE</property>
2692               <property name="cursor_visible">True</property>
2693               <property name="pixels_above_lines">0</property>
2694               <property name="pixels_below_lines">0</property>
2695               <property name="pixels_inside_wrap">0</property>
2696               <property name="left_margin">0</property>
2697               <property name="right_margin">0</property>
2698               <property name="indent">0</property>
2699               <property name="text" translatable="yes"></property>
2700             </widget>
2701           </child>
2702         </widget>
2703         <packing>
2704           <property name="padding">0</property>
2705           <property name="expand">True</property>
2706           <property name="fill">True</property>
2707         </packing>
2708       </child>
2709     </widget>
2710   </child>
2711 </widget>
2712
2713 <widget class="GtkDialog" id="UriChoiceDialog">
2714   <property name="height_request">280</property>
2715   <property name="title" translatable="yes">Uri choice</property>
2716   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2717   <property name="window_position">GTK_WIN_POS_CENTER</property>
2718   <property name="modal">True</property>
2719   <property name="resizable">True</property>
2720   <property name="destroy_with_parent">False</property>
2721   <property name="decorated">True</property>
2722   <property name="skip_taskbar_hint">False</property>
2723   <property name="skip_pager_hint">False</property>
2724   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2725   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2726   <property name="focus_on_map">True</property>
2727   <property name="has_separator">True</property>
2728
2729   <child internal-child="vbox">
2730     <widget class="GtkVBox" id="dialog-vbox3">
2731       <property name="visible">True</property>
2732       <property name="homogeneous">False</property>
2733       <property name="spacing">4</property>
2734
2735       <child internal-child="action_area">
2736         <widget class="GtkHButtonBox" id="dialog-action_area3">
2737           <property name="visible">True</property>
2738           <property name="layout_style">GTK_BUTTONBOX_END</property>
2739
2740           <child>
2741             <widget class="GtkButton" id="UriChoiceAbortButton">
2742               <property name="visible">True</property>
2743               <property name="can_default">True</property>
2744               <property name="can_focus">True</property>
2745               <property name="label">gtk-cancel</property>
2746               <property name="use_stock">True</property>
2747               <property name="relief">GTK_RELIEF_NORMAL</property>
2748               <property name="focus_on_click">True</property>
2749               <property name="response_id">-6</property>
2750             </widget>
2751           </child>
2752
2753           <child>
2754             <widget class="GtkButton" id="UriChoiceSelectedButton">
2755               <property name="visible">True</property>
2756               <property name="can_default">True</property>
2757               <property name="can_focus">True</property>
2758               <property name="relief">GTK_RELIEF_NORMAL</property>
2759               <property name="focus_on_click">True</property>
2760               <property name="response_id">0</property>
2761
2762               <child>
2763                 <widget class="GtkAlignment" id="alignment2">
2764                   <property name="visible">True</property>
2765                   <property name="xalign">0.5</property>
2766                   <property name="yalign">0.5</property>
2767                   <property name="xscale">0</property>
2768                   <property name="yscale">0</property>
2769                   <property name="top_padding">0</property>
2770                   <property name="bottom_padding">0</property>
2771                   <property name="left_padding">0</property>
2772                   <property name="right_padding">0</property>
2773
2774                   <child>
2775                     <widget class="GtkHBox" id="hbox3">
2776                       <property name="visible">True</property>
2777                       <property name="homogeneous">False</property>
2778                       <property name="spacing">2</property>
2779
2780                       <child>
2781                         <widget class="GtkImage" id="image19">
2782                           <property name="visible">True</property>
2783                           <property name="stock">gtk-index</property>
2784                           <property name="icon_size">4</property>
2785                           <property name="xalign">0.5</property>
2786                           <property name="yalign">0.5</property>
2787                           <property name="xpad">0</property>
2788                           <property name="ypad">0</property>
2789                         </widget>
2790                         <packing>
2791                           <property name="padding">0</property>
2792                           <property name="expand">False</property>
2793                           <property name="fill">False</property>
2794                         </packing>
2795                       </child>
2796
2797                       <child>
2798                         <widget class="GtkLabel" id="label3">
2799                           <property name="visible">True</property>
2800                           <property name="label" translatable="yes">Try _Selected</property>
2801                           <property name="use_underline">True</property>
2802                           <property name="use_markup">False</property>
2803                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2804                           <property name="wrap">False</property>
2805                           <property name="selectable">False</property>
2806                           <property name="xalign">0.5</property>
2807                           <property name="yalign">0.5</property>
2808                           <property name="xpad">0</property>
2809                           <property name="ypad">0</property>
2810                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2811                           <property name="width_chars">-1</property>
2812                           <property name="single_line_mode">False</property>
2813                           <property name="angle">0</property>
2814                         </widget>
2815                         <packing>
2816                           <property name="padding">0</property>
2817                           <property name="expand">False</property>
2818                           <property name="fill">False</property>
2819                         </packing>
2820                       </child>
2821                     </widget>
2822                   </child>
2823                 </widget>
2824               </child>
2825             </widget>
2826           </child>
2827
2828           <child>
2829             <widget class="GtkButton" id="UriChoiceConstantsButton">
2830               <property name="visible">True</property>
2831               <property name="sensitive">False</property>
2832               <property name="can_default">True</property>
2833               <property name="can_focus">True</property>
2834               <property name="label" translatable="yes">Try Constants</property>
2835               <property name="use_underline">True</property>
2836               <property name="relief">GTK_RELIEF_NORMAL</property>
2837               <property name="focus_on_click">True</property>
2838               <property name="response_id">0</property>
2839             </widget>
2840           </child>
2841
2842           <child>
2843             <widget class="GtkButton" id="copyButton">
2844               <property name="can_default">True</property>
2845               <property name="can_focus">True</property>
2846               <property name="label">gtk-copy</property>
2847               <property name="use_stock">True</property>
2848               <property name="relief">GTK_RELIEF_NORMAL</property>
2849               <property name="focus_on_click">True</property>
2850               <property name="response_id">0</property>
2851             </widget>
2852           </child>
2853
2854           <child>
2855             <widget class="GtkButton" id="uriChoiceAutoButton">
2856               <property name="visible">True</property>
2857               <property name="can_default">True</property>
2858               <property name="can_focus">True</property>
2859               <property name="relief">GTK_RELIEF_NORMAL</property>
2860               <property name="focus_on_click">True</property>
2861               <property name="response_id">0</property>
2862
2863               <child>
2864                 <widget class="GtkAlignment" id="alignment5">
2865                   <property name="visible">True</property>
2866                   <property name="xalign">0.5</property>
2867                   <property name="yalign">0.5</property>
2868                   <property name="xscale">0</property>
2869                   <property name="yscale">0</property>
2870                   <property name="top_padding">0</property>
2871                   <property name="bottom_padding">0</property>
2872                   <property name="left_padding">0</property>
2873                   <property name="right_padding">0</property>
2874
2875                   <child>
2876                     <widget class="GtkHBox" id="hbox16">
2877                       <property name="visible">True</property>
2878                       <property name="homogeneous">False</property>
2879                       <property name="spacing">2</property>
2880
2881                       <child>
2882                         <widget class="GtkImage" id="image302">
2883                           <property name="visible">True</property>
2884                           <property name="stock">gtk-ok</property>
2885                           <property name="icon_size">4</property>
2886                           <property name="xalign">0.5</property>
2887                           <property name="yalign">0.5</property>
2888                           <property name="xpad">0</property>
2889                           <property name="ypad">0</property>
2890                         </widget>
2891                         <packing>
2892                           <property name="padding">0</property>
2893                           <property name="expand">False</property>
2894                           <property name="fill">False</property>
2895                         </packing>
2896                       </child>
2897
2898                       <child>
2899                         <widget class="GtkLabel" id="okLabel">
2900                           <property name="visible">True</property>
2901                           <property name="label" translatable="yes">bla bla bla</property>
2902                           <property name="use_underline">True</property>
2903                           <property name="use_markup">False</property>
2904                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2905                           <property name="wrap">False</property>
2906                           <property name="selectable">False</property>
2907                           <property name="xalign">0.5</property>
2908                           <property name="yalign">0.5</property>
2909                           <property name="xpad">0</property>
2910                           <property name="ypad">0</property>
2911                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2912                           <property name="width_chars">-1</property>
2913                           <property name="single_line_mode">False</property>
2914                           <property name="angle">0</property>
2915                         </widget>
2916                         <packing>
2917                           <property name="padding">0</property>
2918                           <property name="expand">False</property>
2919                           <property name="fill">False</property>
2920                         </packing>
2921                       </child>
2922                     </widget>
2923                   </child>
2924                 </widget>
2925               </child>
2926             </widget>
2927           </child>
2928         </widget>
2929         <packing>
2930           <property name="padding">0</property>
2931           <property name="expand">False</property>
2932           <property name="fill">True</property>
2933           <property name="pack_type">GTK_PACK_END</property>
2934         </packing>
2935       </child>
2936
2937       <child>
2938         <widget class="GtkVBox" id="vbox2">
2939           <property name="visible">True</property>
2940           <property name="homogeneous">False</property>
2941           <property name="spacing">3</property>
2942
2943           <child>
2944             <widget class="GtkLabel" id="UriChoiceLabel">
2945               <property name="visible">True</property>
2946               <property name="label" translatable="yes">some informative message here ...</property>
2947               <property name="use_underline">False</property>
2948               <property name="use_markup">False</property>
2949               <property name="justify">GTK_JUSTIFY_LEFT</property>
2950               <property name="wrap">False</property>
2951               <property name="selectable">False</property>
2952               <property name="xalign">0.5</property>
2953               <property name="yalign">0.5</property>
2954               <property name="xpad">0</property>
2955               <property name="ypad">0</property>
2956               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
2957               <property name="width_chars">-1</property>
2958               <property name="single_line_mode">False</property>
2959               <property name="angle">0</property>
2960             </widget>
2961             <packing>
2962               <property name="padding">0</property>
2963               <property name="expand">False</property>
2964               <property name="fill">False</property>
2965             </packing>
2966           </child>
2967
2968           <child>
2969             <widget class="GtkScrolledWindow" id="scrolledwindow1">
2970               <property name="width_request">400</property>
2971               <property name="visible">True</property>
2972               <property name="can_focus">True</property>
2973               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2974               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2975               <property name="shadow_type">GTK_SHADOW_NONE</property>
2976               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2977
2978               <child>
2979                 <widget class="GtkTreeView" id="UriChoiceTreeView">
2980                   <property name="visible">True</property>
2981                   <property name="can_focus">True</property>
2982                   <property name="headers_visible">False</property>
2983                   <property name="rules_hint">False</property>
2984                   <property name="reorderable">False</property>
2985                   <property name="enable_search">True</property>
2986                   <property name="fixed_height_mode">False</property>
2987                   <property name="hover_selection">False</property>
2988                   <property name="hover_expand">False</property>
2989                 </widget>
2990               </child>
2991             </widget>
2992             <packing>
2993               <property name="padding">0</property>
2994               <property name="expand">True</property>
2995               <property name="fill">True</property>
2996             </packing>
2997           </child>
2998
2999           <child>
3000             <widget class="GtkHBox" id="uriEntryHBox">
3001               <property name="visible">True</property>
3002               <property name="homogeneous">False</property>
3003               <property name="spacing">0</property>
3004
3005               <child>
3006                 <widget class="GtkLabel" id="label2">
3007                   <property name="visible">True</property>
3008                   <property name="label" translatable="yes">URI: </property>
3009                   <property name="use_underline">False</property>
3010                   <property name="use_markup">False</property>
3011                   <property name="justify">GTK_JUSTIFY_LEFT</property>
3012                   <property name="wrap">False</property>
3013                   <property name="selectable">False</property>
3014                   <property name="xalign">0.5</property>
3015                   <property name="yalign">0.5</property>
3016                   <property name="xpad">0</property>
3017                   <property name="ypad">0</property>
3018                   <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3019                   <property name="width_chars">-1</property>
3020                   <property name="single_line_mode">False</property>
3021                   <property name="angle">0</property>
3022                 </widget>
3023                 <packing>
3024                   <property name="padding">0</property>
3025                   <property name="expand">False</property>
3026                   <property name="fill">False</property>
3027                 </packing>
3028               </child>
3029
3030               <child>
3031                 <widget class="GtkEntry" id="entry1">
3032                   <property name="visible">True</property>
3033                   <property name="can_focus">True</property>
3034                   <property name="editable">True</property>
3035                   <property name="visibility">True</property>
3036                   <property name="max_length">0</property>
3037                   <property name="text" translatable="yes"></property>
3038                   <property name="has_frame">True</property>
3039                   <property name="invisible_char">*</property>
3040                   <property name="activates_default">False</property>
3041                 </widget>
3042                 <packing>
3043                   <property name="padding">0</property>
3044                   <property name="expand">True</property>
3045                   <property name="fill">True</property>
3046                 </packing>
3047               </child>
3048             </widget>
3049             <packing>
3050               <property name="padding">0</property>
3051               <property name="expand">False</property>
3052               <property name="fill">True</property>
3053             </packing>
3054           </child>
3055         </widget>
3056         <packing>
3057           <property name="padding">0</property>
3058           <property name="expand">True</property>
3059           <property name="fill">True</property>
3060         </packing>
3061       </child>
3062     </widget>
3063   </child>
3064 </widget>
3065
3066 <widget class="GtkWindow" id="FindReplWin">
3067   <property name="border_width">5</property>
3068   <property name="title" translatable="yes">Find &amp; Replace</property>
3069   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3070   <property name="window_position">GTK_WIN_POS_MOUSE</property>
3071   <property name="modal">False</property>
3072   <property name="resizable">False</property>
3073   <property name="destroy_with_parent">False</property>
3074   <property name="decorated">True</property>
3075   <property name="skip_taskbar_hint">False</property>
3076   <property name="skip_pager_hint">False</property>
3077   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
3078   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3079   <property name="focus_on_map">True</property>
3080
3081   <child>
3082     <widget class="GtkTable" id="table1">
3083       <property name="visible">True</property>
3084       <property name="n_rows">3</property>
3085       <property name="n_columns">2</property>
3086       <property name="homogeneous">False</property>
3087       <property name="row_spacing">5</property>
3088       <property name="column_spacing">0</property>
3089
3090       <child>
3091         <widget class="GtkLabel" id="label17">
3092           <property name="visible">True</property>
3093           <property name="label" translatable="yes">Find:</property>
3094           <property name="use_underline">False</property>
3095           <property name="use_markup">False</property>
3096           <property name="justify">GTK_JUSTIFY_LEFT</property>
3097           <property name="wrap">False</property>
3098           <property name="selectable">False</property>
3099           <property name="xalign">0</property>
3100           <property name="yalign">0.5</property>
3101           <property name="xpad">0</property>
3102           <property name="ypad">0</property>
3103           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3104           <property name="width_chars">-1</property>
3105           <property name="single_line_mode">False</property>
3106           <property name="angle">0</property>
3107         </widget>
3108         <packing>
3109           <property name="left_attach">0</property>
3110           <property name="right_attach">1</property>
3111           <property name="top_attach">0</property>
3112           <property name="bottom_attach">1</property>
3113           <property name="x_options">fill</property>
3114           <property name="y_options"></property>
3115         </packing>
3116       </child>
3117
3118       <child>
3119         <widget class="GtkLabel" id="label18">
3120           <property name="visible">True</property>
3121           <property name="label" translatable="yes">Replace with: </property>
3122           <property name="use_underline">False</property>
3123           <property name="use_markup">False</property>
3124           <property name="justify">GTK_JUSTIFY_LEFT</property>
3125           <property name="wrap">False</property>
3126           <property name="selectable">False</property>
3127           <property name="xalign">0</property>
3128           <property name="yalign">0.5</property>
3129           <property name="xpad">0</property>
3130           <property name="ypad">0</property>
3131           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3132           <property name="width_chars">-1</property>
3133           <property name="single_line_mode">False</property>
3134           <property name="angle">0</property>
3135         </widget>
3136         <packing>
3137           <property name="left_attach">0</property>
3138           <property name="right_attach">1</property>
3139           <property name="top_attach">1</property>
3140           <property name="bottom_attach">2</property>
3141           <property name="x_options">fill</property>
3142           <property name="y_options"></property>
3143         </packing>
3144       </child>
3145
3146       <child>
3147         <widget class="GtkEntry" id="findEntry">
3148           <property name="visible">True</property>
3149           <property name="can_default">True</property>
3150           <property name="has_default">True</property>
3151           <property name="can_focus">True</property>
3152           <property name="has_focus">True</property>
3153           <property name="editable">True</property>
3154           <property name="visibility">True</property>
3155           <property name="max_length">0</property>
3156           <property name="text" translatable="yes"></property>
3157           <property name="has_frame">True</property>
3158           <property name="invisible_char">*</property>
3159           <property name="activates_default">False</property>
3160         </widget>
3161         <packing>
3162           <property name="left_attach">1</property>
3163           <property name="right_attach">2</property>
3164           <property name="top_attach">0</property>
3165           <property name="bottom_attach">1</property>
3166           <property name="y_options"></property>
3167         </packing>
3168       </child>
3169
3170       <child>
3171         <widget class="GtkEntry" id="replaceEntry">
3172           <property name="visible">True</property>
3173           <property name="can_focus">True</property>
3174           <property name="editable">True</property>
3175           <property name="visibility">True</property>
3176           <property name="max_length">0</property>
3177           <property name="text" translatable="yes"></property>
3178           <property name="has_frame">True</property>
3179           <property name="invisible_char">*</property>
3180           <property name="activates_default">False</property>
3181         </widget>
3182         <packing>
3183           <property name="left_attach">1</property>
3184           <property name="right_attach">2</property>
3185           <property name="top_attach">1</property>
3186           <property name="bottom_attach">2</property>
3187           <property name="y_options"></property>
3188         </packing>
3189       </child>
3190
3191       <child>
3192         <widget class="GtkHBox" id="hbox19">
3193           <property name="visible">True</property>
3194           <property name="homogeneous">False</property>
3195           <property name="spacing">5</property>
3196
3197           <child>
3198             <widget class="GtkVBox" id="vbox9">
3199               <property name="visible">True</property>
3200               <property name="homogeneous">False</property>
3201               <property name="spacing">0</property>
3202
3203               <child>
3204                 <placeholder/>
3205               </child>
3206
3207               <child>
3208                 <placeholder/>
3209               </child>
3210             </widget>
3211             <packing>
3212               <property name="padding">0</property>
3213               <property name="expand">True</property>
3214               <property name="fill">True</property>
3215             </packing>
3216           </child>
3217
3218           <child>
3219             <widget class="GtkButton" id="findButton">
3220               <property name="visible">True</property>
3221               <property name="can_focus">True</property>
3222               <property name="label">gtk-find</property>
3223               <property name="use_stock">True</property>
3224               <property name="relief">GTK_RELIEF_NORMAL</property>
3225               <property name="focus_on_click">True</property>
3226             </widget>
3227             <packing>
3228               <property name="padding">0</property>
3229               <property name="expand">False</property>
3230               <property name="fill">False</property>
3231             </packing>
3232           </child>
3233
3234           <child>
3235             <widget class="GtkButton" id="findReplButton">
3236               <property name="visible">True</property>
3237               <property name="can_focus">True</property>
3238               <property name="relief">GTK_RELIEF_NORMAL</property>
3239               <property name="focus_on_click">True</property>
3240
3241               <child>
3242                 <widget class="GtkAlignment" id="alignment13">
3243                   <property name="visible">True</property>
3244                   <property name="xalign">0.5</property>
3245                   <property name="yalign">0.5</property>
3246                   <property name="xscale">0</property>
3247                   <property name="yscale">0</property>
3248                   <property name="top_padding">0</property>
3249                   <property name="bottom_padding">0</property>
3250                   <property name="left_padding">0</property>
3251                   <property name="right_padding">0</property>
3252
3253                   <child>
3254                     <widget class="GtkHBox" id="hbox20">
3255                       <property name="visible">True</property>
3256                       <property name="homogeneous">False</property>
3257                       <property name="spacing">2</property>
3258
3259                       <child>
3260                         <widget class="GtkImage" id="image357">
3261                           <property name="visible">True</property>
3262                           <property name="stock">gtk-find-and-replace</property>
3263                           <property name="icon_size">4</property>
3264                           <property name="xalign">0.5</property>
3265                           <property name="yalign">0.5</property>
3266                           <property name="xpad">0</property>
3267                           <property name="ypad">0</property>
3268                         </widget>
3269                         <packing>
3270                           <property name="padding">0</property>
3271                           <property name="expand">False</property>
3272                           <property name="fill">False</property>
3273                         </packing>
3274                       </child>
3275
3276                       <child>
3277                         <widget class="GtkLabel" id="label19">
3278                           <property name="visible">True</property>
3279                           <property name="label">_Replace</property>
3280                           <property name="use_underline">True</property>
3281                           <property name="use_markup">False</property>
3282                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3283                           <property name="wrap">False</property>
3284                           <property name="selectable">False</property>
3285                           <property name="xalign">0.5</property>
3286                           <property name="yalign">0.5</property>
3287                           <property name="xpad">0</property>
3288                           <property name="ypad">0</property>
3289                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3290                           <property name="width_chars">-1</property>
3291                           <property name="single_line_mode">False</property>
3292                           <property name="angle">0</property>
3293                         </widget>
3294                         <packing>
3295                           <property name="padding">0</property>
3296                           <property name="expand">False</property>
3297                           <property name="fill">False</property>
3298                         </packing>
3299                       </child>
3300                     </widget>
3301                   </child>
3302                 </widget>
3303               </child>
3304             </widget>
3305             <packing>
3306               <property name="padding">0</property>
3307               <property name="expand">False</property>
3308               <property name="fill">False</property>
3309             </packing>
3310           </child>
3311
3312           <child>
3313             <widget class="GtkButton" id="cancelButton">
3314               <property name="visible">True</property>
3315               <property name="can_focus">True</property>
3316               <property name="label">gtk-cancel</property>
3317               <property name="use_stock">True</property>
3318               <property name="relief">GTK_RELIEF_NORMAL</property>
3319               <property name="focus_on_click">True</property>
3320             </widget>
3321             <packing>
3322               <property name="padding">0</property>
3323               <property name="expand">False</property>
3324               <property name="fill">False</property>
3325             </packing>
3326           </child>
3327         </widget>
3328         <packing>
3329           <property name="left_attach">0</property>
3330           <property name="right_attach">2</property>
3331           <property name="top_attach">2</property>
3332           <property name="bottom_attach">3</property>
3333           <property name="y_padding">5</property>
3334         </packing>
3335       </child>
3336     </widget>
3337   </child>
3338 </widget>
3339
3340 <widget class="GtkWindow" id="NewDevelWin">
3341   <property name="title" translatable="yes">Create development</property>
3342   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3343   <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
3344   <property name="modal">True</property>
3345   <property name="resizable">False</property>
3346   <property name="destroy_with_parent">False</property>
3347   <property name="decorated">True</property>
3348   <property name="skip_taskbar_hint">False</property>
3349   <property name="skip_pager_hint">False</property>
3350   <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
3351   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3352   <property name="focus_on_map">True</property>
3353
3354   <child>
3355     <widget class="GtkVBox" id="vbox10">
3356       <property name="visible">True</property>
3357       <property name="homogeneous">False</property>
3358       <property name="spacing">0</property>
3359
3360       <child>
3361         <widget class="GtkTable" id="table2">
3362           <property name="border_width">3</property>
3363           <property name="visible">True</property>
3364           <property name="n_rows">2</property>
3365           <property name="n_columns">3</property>
3366           <property name="homogeneous">False</property>
3367           <property name="row_spacing">5</property>
3368           <property name="column_spacing">5</property>
3369
3370           <child>
3371             <widget class="GtkLabel" id="label20">
3372               <property name="visible">True</property>
3373               <property name="label" translatable="yes">Name</property>
3374               <property name="use_underline">False</property>
3375               <property name="use_markup">False</property>
3376               <property name="justify">GTK_JUSTIFY_LEFT</property>
3377               <property name="wrap">False</property>
3378               <property name="selectable">False</property>
3379               <property name="xalign">0</property>
3380               <property name="yalign">0.5</property>
3381               <property name="xpad">0</property>
3382               <property name="ypad">0</property>
3383               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3384               <property name="width_chars">-1</property>
3385               <property name="single_line_mode">False</property>
3386               <property name="angle">0</property>
3387             </widget>
3388             <packing>
3389               <property name="left_attach">0</property>
3390               <property name="right_attach">1</property>
3391               <property name="top_attach">0</property>
3392               <property name="bottom_attach">1</property>
3393               <property name="x_options">fill</property>
3394               <property name="y_options"></property>
3395             </packing>
3396           </child>
3397
3398           <child>
3399             <widget class="GtkLabel" id="label21">
3400               <property name="visible">True</property>
3401               <property name="label" translatable="yes">Root directory</property>
3402               <property name="use_underline">False</property>
3403               <property name="use_markup">False</property>
3404               <property name="justify">GTK_JUSTIFY_LEFT</property>
3405               <property name="wrap">False</property>
3406               <property name="selectable">False</property>
3407               <property name="xalign">0</property>
3408               <property name="yalign">0.5</property>
3409               <property name="xpad">0</property>
3410               <property name="ypad">0</property>
3411               <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3412               <property name="width_chars">-1</property>
3413               <property name="single_line_mode">False</property>
3414               <property name="angle">0</property>
3415             </widget>
3416             <packing>
3417               <property name="left_attach">0</property>
3418               <property name="right_attach">1</property>
3419               <property name="top_attach">1</property>
3420               <property name="bottom_attach">2</property>
3421               <property name="x_options">fill</property>
3422               <property name="y_options"></property>
3423             </packing>
3424           </child>
3425
3426           <child>
3427             <widget class="GtkEntry" id="nameEntry">
3428               <property name="visible">True</property>
3429               <property name="can_focus">True</property>
3430               <property name="editable">True</property>
3431               <property name="visibility">True</property>
3432               <property name="max_length">0</property>
3433               <property name="text" translatable="yes"></property>
3434               <property name="has_frame">True</property>
3435               <property name="invisible_char">*</property>
3436               <property name="activates_default">False</property>
3437             </widget>
3438             <packing>
3439               <property name="left_attach">1</property>
3440               <property name="right_attach">2</property>
3441               <property name="top_attach">0</property>
3442               <property name="bottom_attach">1</property>
3443               <property name="y_options"></property>
3444             </packing>
3445           </child>
3446
3447           <child>
3448             <widget class="GtkEntry" id="rootEntry">
3449               <property name="visible">True</property>
3450               <property name="can_focus">True</property>
3451               <property name="editable">True</property>
3452               <property name="visibility">True</property>
3453               <property name="max_length">0</property>
3454               <property name="text" translatable="yes"></property>
3455               <property name="has_frame">True</property>
3456               <property name="invisible_char">*</property>
3457               <property name="activates_default">False</property>
3458             </widget>
3459             <packing>
3460               <property name="left_attach">1</property>
3461               <property name="right_attach">2</property>
3462               <property name="top_attach">1</property>
3463               <property name="bottom_attach">2</property>
3464               <property name="y_options"></property>
3465             </packing>
3466           </child>
3467
3468           <child>
3469             <widget class="GtkButton" id="chooseRootButton">
3470               <property name="visible">True</property>
3471               <property name="can_focus">True</property>
3472               <property name="label" translatable="yes">...</property>
3473               <property name="use_underline">True</property>
3474               <property name="relief">GTK_RELIEF_NORMAL</property>
3475               <property name="focus_on_click">True</property>
3476             </widget>
3477             <packing>
3478               <property name="left_attach">2</property>
3479               <property name="right_attach">3</property>
3480               <property name="top_attach">1</property>
3481               <property name="bottom_attach">2</property>
3482               <property name="x_options">fill</property>
3483               <property name="y_options"></property>
3484             </packing>
3485           </child>
3486         </widget>
3487         <packing>
3488           <property name="padding">0</property>
3489           <property name="expand">False</property>
3490           <property name="fill">True</property>
3491         </packing>
3492       </child>
3493
3494       <child>
3495         <widget class="GtkHSeparator" id="hseparator1">
3496           <property name="visible">True</property>
3497         </widget>
3498         <packing>
3499           <property name="padding">2</property>
3500           <property name="expand">False</property>
3501           <property name="fill">True</property>
3502         </packing>
3503       </child>
3504
3505       <child>
3506         <widget class="GtkHBox" id="hbox21">
3507           <property name="border_width">3</property>
3508           <property name="visible">True</property>
3509           <property name="homogeneous">False</property>
3510           <property name="spacing">5</property>
3511
3512           <child>
3513             <widget class="GtkVBox" id="vbox11">
3514               <property name="visible">True</property>
3515               <property name="homogeneous">False</property>
3516               <property name="spacing">0</property>
3517
3518               <child>
3519                 <placeholder/>
3520               </child>
3521
3522               <child>
3523                 <placeholder/>
3524               </child>
3525             </widget>
3526             <packing>
3527               <property name="padding">0</property>
3528               <property name="expand">True</property>
3529               <property name="fill">True</property>
3530             </packing>
3531           </child>
3532
3533           <child>
3534             <widget class="GtkButton" id="addButton">
3535               <property name="visible">True</property>
3536               <property name="can_focus">True</property>
3537               <property name="label">gtk-add</property>
3538               <property name="use_stock">True</property>
3539               <property name="relief">GTK_RELIEF_NORMAL</property>
3540               <property name="focus_on_click">True</property>
3541             </widget>
3542             <packing>
3543               <property name="padding">0</property>
3544               <property name="expand">False</property>
3545               <property name="fill">False</property>
3546             </packing>
3547           </child>
3548
3549           <child>
3550             <widget class="GtkButton" id="cancelButton">
3551               <property name="visible">True</property>
3552               <property name="can_focus">True</property>
3553               <property name="label">gtk-cancel</property>
3554               <property name="use_stock">True</property>
3555               <property name="relief">GTK_RELIEF_NORMAL</property>
3556               <property name="focus_on_click">True</property>
3557             </widget>
3558             <packing>
3559               <property name="padding">0</property>
3560               <property name="expand">False</property>
3561               <property name="fill">False</property>
3562             </packing>
3563           </child>
3564         </widget>
3565         <packing>
3566           <property name="padding">0</property>
3567           <property name="expand">False</property>
3568           <property name="fill">True</property>
3569         </packing>
3570       </child>
3571     </widget>
3572   </child>
3573 </widget>
3574
3575 <widget class="GtkWindow" id="DevelListWin">
3576   <property name="title" translatable="yes">Developments</property>
3577   <property name="type">GTK_WINDOW_TOPLEVEL</property>
3578   <property name="window_position">GTK_WIN_POS_CENTER</property>
3579   <property name="modal">False</property>
3580   <property name="resizable">True</property>
3581   <property name="destroy_with_parent">False</property>
3582   <property name="decorated">True</property>
3583   <property name="skip_taskbar_hint">False</property>
3584   <property name="skip_pager_hint">False</property>
3585   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
3586   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
3587   <property name="focus_on_map">True</property>
3588
3589   <child>
3590     <widget class="GtkVBox" id="vbox12">
3591       <property name="visible">True</property>
3592       <property name="homogeneous">False</property>
3593       <property name="spacing">0</property>
3594
3595       <child>
3596         <widget class="GtkScrolledWindow" id="scrolledwindow10">
3597           <property name="visible">True</property>
3598           <property name="can_focus">True</property>
3599           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3600           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
3601           <property name="shadow_type">GTK_SHADOW_IN</property>
3602           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
3603
3604           <child>
3605             <widget class="GtkTreeView" id="developmentsTreeview">
3606               <property name="visible">True</property>
3607               <property name="can_focus">True</property>
3608               <property name="headers_visible">False</property>
3609               <property name="rules_hint">False</property>
3610               <property name="reorderable">False</property>
3611               <property name="enable_search">True</property>
3612               <property name="fixed_height_mode">False</property>
3613               <property name="hover_selection">False</property>
3614               <property name="hover_expand">False</property>
3615             </widget>
3616           </child>
3617         </widget>
3618         <packing>
3619           <property name="padding">0</property>
3620           <property name="expand">True</property>
3621           <property name="fill">True</property>
3622         </packing>
3623       </child>
3624
3625       <child>
3626         <widget class="GtkHSeparator" id="hseparator2">
3627           <property name="visible">True</property>
3628         </widget>
3629         <packing>
3630           <property name="padding">2</property>
3631           <property name="expand">False</property>
3632           <property name="fill">True</property>
3633         </packing>
3634       </child>
3635
3636       <child>
3637         <widget class="GtkHBox" id="buttonsHbox">
3638           <property name="border_width">3</property>
3639           <property name="visible">True</property>
3640           <property name="homogeneous">False</property>
3641           <property name="spacing">4</property>
3642
3643           <child>
3644             <widget class="GtkVBox" id="vbox13">
3645               <property name="visible">True</property>
3646               <property name="homogeneous">False</property>
3647               <property name="spacing">0</property>
3648
3649               <child>
3650                 <placeholder/>
3651               </child>
3652
3653               <child>
3654                 <placeholder/>
3655               </child>
3656             </widget>
3657             <packing>
3658               <property name="padding">0</property>
3659               <property name="expand">True</property>
3660               <property name="fill">True</property>
3661             </packing>
3662           </child>
3663
3664           <child>
3665             <widget class="GtkButton" id="newButton">
3666               <property name="visible">True</property>
3667               <property name="can_focus">True</property>
3668               <property name="label">gtk-new</property>
3669               <property name="use_stock">True</property>
3670               <property name="relief">GTK_RELIEF_NORMAL</property>
3671               <property name="focus_on_click">True</property>
3672             </widget>
3673             <packing>
3674               <property name="padding">0</property>
3675               <property name="expand">False</property>
3676               <property name="fill">False</property>
3677             </packing>
3678           </child>
3679
3680           <child>
3681             <widget class="GtkButton" id="deleteButton">
3682               <property name="visible">True</property>
3683               <property name="can_focus">True</property>
3684               <property name="label">gtk-delete</property>
3685               <property name="use_stock">True</property>
3686               <property name="relief">GTK_RELIEF_NORMAL</property>
3687               <property name="focus_on_click">True</property>
3688             </widget>
3689             <packing>
3690               <property name="padding">0</property>
3691               <property name="expand">False</property>
3692               <property name="fill">False</property>
3693             </packing>
3694           </child>
3695
3696           <child>
3697             <widget class="GtkButton" id="buildButton">
3698               <property name="visible">True</property>
3699               <property name="can_focus">True</property>
3700               <property name="relief">GTK_RELIEF_NORMAL</property>
3701               <property name="focus_on_click">True</property>
3702
3703               <child>
3704                 <widget class="GtkAlignment" id="alignment14">
3705                   <property name="visible">True</property>
3706                   <property name="xalign">0.5</property>
3707                   <property name="yalign">0.5</property>
3708                   <property name="xscale">0</property>
3709                   <property name="yscale">0</property>
3710                   <property name="top_padding">0</property>
3711                   <property name="bottom_padding">0</property>
3712                   <property name="left_padding">0</property>
3713                   <property name="right_padding">0</property>
3714
3715                   <child>
3716                     <widget class="GtkHBox" id="hbox23">
3717                       <property name="visible">True</property>
3718                       <property name="homogeneous">False</property>
3719                       <property name="spacing">2</property>
3720
3721                       <child>
3722                         <widget class="GtkImage" id="image358">
3723                           <property name="visible">True</property>
3724                           <property name="stock">gtk-execute</property>
3725                           <property name="icon_size">4</property>
3726                           <property name="xalign">0.5</property>
3727                           <property name="yalign">0.5</property>
3728                           <property name="xpad">0</property>
3729                           <property name="ypad">0</property>
3730                         </widget>
3731                         <packing>
3732                           <property name="padding">0</property>
3733                           <property name="expand">False</property>
3734                           <property name="fill">False</property>
3735                         </packing>
3736                       </child>
3737
3738                       <child>
3739                         <widget class="GtkLabel" id="label22">
3740                           <property name="visible">True</property>
3741                           <property name="label" translatable="yes">_Build</property>
3742                           <property name="use_underline">True</property>
3743                           <property name="use_markup">False</property>
3744                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3745                           <property name="wrap">False</property>
3746                           <property name="selectable">False</property>
3747                           <property name="xalign">0.5</property>
3748                           <property name="yalign">0.5</property>
3749                           <property name="xpad">0</property>
3750                           <property name="ypad">0</property>
3751                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3752                           <property name="width_chars">-1</property>
3753                           <property name="single_line_mode">False</property>
3754                           <property name="angle">0</property>
3755                         </widget>
3756                         <packing>
3757                           <property name="padding">0</property>
3758                           <property name="expand">False</property>
3759                           <property name="fill">False</property>
3760                         </packing>
3761                       </child>
3762                     </widget>
3763                   </child>
3764                 </widget>
3765               </child>
3766             </widget>
3767             <packing>
3768               <property name="padding">0</property>
3769               <property name="expand">False</property>
3770               <property name="fill">False</property>
3771             </packing>
3772           </child>
3773
3774           <child>
3775             <widget class="GtkButton" id="cleanButton">
3776               <property name="visible">True</property>
3777               <property name="can_focus">True</property>
3778               <property name="relief">GTK_RELIEF_NORMAL</property>
3779               <property name="focus_on_click">True</property>
3780
3781               <child>
3782                 <widget class="GtkAlignment" id="alignment15">
3783                   <property name="visible">True</property>
3784                   <property name="xalign">0.5</property>
3785                   <property name="yalign">0.5</property>
3786                   <property name="xscale">0</property>
3787                   <property name="yscale">0</property>
3788                   <property name="top_padding">0</property>
3789                   <property name="bottom_padding">0</property>
3790                   <property name="left_padding">0</property>
3791                   <property name="right_padding">0</property>
3792
3793                   <child>
3794                     <widget class="GtkHBox" id="hbox24">
3795                       <property name="visible">True</property>
3796                       <property name="homogeneous">False</property>
3797                       <property name="spacing">2</property>
3798
3799                       <child>
3800                         <widget class="GtkImage" id="image359">
3801                           <property name="visible">True</property>
3802                           <property name="stock">gtk-clear</property>
3803                           <property name="icon_size">4</property>
3804                           <property name="xalign">0.5</property>
3805                           <property name="yalign">0.5</property>
3806                           <property name="xpad">0</property>
3807                           <property name="ypad">0</property>
3808                         </widget>
3809                         <packing>
3810                           <property name="padding">0</property>
3811                           <property name="expand">False</property>
3812                           <property name="fill">False</property>
3813                         </packing>
3814                       </child>
3815
3816                       <child>
3817                         <widget class="GtkLabel" id="label23">
3818                           <property name="visible">True</property>
3819                           <property name="label" translatable="yes">C_lean</property>
3820                           <property name="use_underline">True</property>
3821                           <property name="use_markup">False</property>
3822                           <property name="justify">GTK_JUSTIFY_LEFT</property>
3823                           <property name="wrap">False</property>
3824                           <property name="selectable">False</property>
3825                           <property name="xalign">0.5</property>
3826                           <property name="yalign">0.5</property>
3827                           <property name="xpad">0</property>
3828                           <property name="ypad">0</property>
3829                           <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
3830                           <property name="width_chars">-1</property>
3831                           <property name="single_line_mode">False</property>
3832                           <property name="angle">0</property>
3833                         </widget>
3834                         <packing>
3835                           <property name="padding">0</property>
3836                           <property name="expand">False</property>
3837                           <property name="fill">False</property>
3838                         </packing>
3839                       </child>
3840                     </widget>
3841                   </child>
3842                 </widget>
3843               </child>
3844             </widget>
3845             <packing>
3846               <property name="padding">0</property>
3847               <property name="expand">False</property>
3848               <property name="fill">False</property>
3849             </packing>
3850           </child>
3851
3852           <child>
3853             <widget class="GtkButton" id="closeButton">
3854               <property name="visible">True</property>
3855               <property name="can_focus">True</property>
3856               <property name="label">gtk-close</property>
3857               <property name="use_stock">True</property>
3858               <property name="relief">GTK_RELIEF_NORMAL</property>
3859               <property name="focus_on_click">True</property>
3860             </widget>
3861             <packing>
3862               <property name="padding">0</property>
3863               <property name="expand">False</property>
3864               <property name="fill">False</property>
3865             </packing>
3866           </child>
3867         </widget>
3868         <packing>
3869           <property name="padding">0</property>
3870           <property name="expand">False</property>
3871           <property name="fill">True</property>
3872         </packing>
3873       </child>
3874     </widget>
3875   </child>
3876 </widget>
3877
3878 </glade-interface>