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