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