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