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