]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matita.glade
bugfix: "LPAREN" vs LPAREN
[helm.git] / helm / matita / matita.glade
1 <?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
2 <!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
3
4 <glade-interface>
5
6 <widget class="GtkDialog" id="AboutWin">
7   <property name="title" translatable="yes">Matita: about</property>
8   <property name="type">GTK_WINDOW_TOPLEVEL</property>
9   <property name="window_position">GTK_WIN_POS_CENTER</property>
10   <property name="modal">True</property>
11   <property name="resizable">False</property>
12   <property name="destroy_with_parent">False</property>
13   <property name="decorated">True</property>
14   <property name="skip_taskbar_hint">False</property>
15   <property name="skip_pager_hint">False</property>
16   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
17   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
18   <property name="has_separator">True</property>
19
20   <child internal-child="vbox">
21     <widget class="GtkVBox" id="dialog-vbox2">
22       <property name="visible">True</property>
23       <property name="homogeneous">False</property>
24       <property name="spacing">0</property>
25
26       <child internal-child="action_area">
27         <widget class="GtkHButtonBox" id="dialog-action_area2">
28           <property name="visible">True</property>
29           <property name="layout_style">GTK_BUTTONBOX_END</property>
30
31           <child>
32             <widget class="GtkButton" id="AboutDismissButton">
33               <property name="visible">True</property>
34               <property name="can_default">True</property>
35               <property name="can_focus">True</property>
36               <property name="label">gtk-ok</property>
37               <property name="use_stock">True</property>
38               <property name="relief">GTK_RELIEF_NORMAL</property>
39               <property name="focus_on_click">True</property>
40               <property name="response_id">-5</property>
41             </widget>
42           </child>
43         </widget>
44         <packing>
45           <property name="padding">0</property>
46           <property name="expand">False</property>
47           <property name="fill">True</property>
48           <property name="pack_type">GTK_PACK_END</property>
49         </packing>
50       </child>
51
52       <child>
53         <widget class="GtkLabel" id="AboutLabel">
54           <property name="visible">True</property>
55           <property name="label" translatable="yes">&lt;b&gt;Matita @VERSION@&lt;/b&gt;
56
57 &lt;tt&gt;http://helm.cs.unibo.it&lt;/tt&gt;
58
59 Copyright (C) 2005,
60 &lt;i&gt;the HELM team&lt;/i&gt;</property>
61           <property name="use_underline">False</property>
62           <property name="use_markup">True</property>
63           <property name="justify">GTK_JUSTIFY_CENTER</property>
64           <property name="wrap">False</property>
65           <property name="selectable">False</property>
66           <property name="xalign">0.5</property>
67           <property name="yalign">0.5</property>
68           <property name="xpad">5</property>
69           <property name="ypad">5</property>
70         </widget>
71         <packing>
72           <property name="padding">0</property>
73           <property name="expand">False</property>
74           <property name="fill">False</property>
75         </packing>
76       </child>
77     </widget>
78   </child>
79 </widget>
80
81 <widget class="GtkWindow" id="BrowserWin">
82   <property name="visible">True</property>
83   <property name="title" translatable="yes">Cic browser</property>
84   <property name="type">GTK_WINDOW_TOPLEVEL</property>
85   <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
86   <property name="modal">False</property>
87   <property name="default_width">500</property>
88   <property name="default_height">500</property>
89   <property name="resizable">True</property>
90   <property name="destroy_with_parent">False</property>
91   <property name="decorated">True</property>
92   <property name="skip_taskbar_hint">False</property>
93   <property name="skip_pager_hint">False</property>
94   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
95   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
96
97   <child>
98     <widget class="GtkEventBox" id="BrowserWinEventBox">
99       <property name="visible">True</property>
100       <property name="visible_window">True</property>
101       <property name="above_child">False</property>
102
103       <child>
104         <widget class="GtkVBox" id="BrowserVBox">
105           <property name="visible">True</property>
106           <property name="homogeneous">False</property>
107           <property name="spacing">0</property>
108
109           <child>
110             <widget class="GtkFrame" id="frame2">
111               <property name="visible">True</property>
112               <property name="label_xalign">0</property>
113               <property name="label_yalign">0</property>
114               <property name="shadow_type">GTK_SHADOW_NONE</property>
115
116               <child>
117                 <widget class="GtkHBox" id="BrowserHBox">
118                   <property name="visible">True</property>
119                   <property name="homogeneous">False</property>
120                   <property name="spacing">0</property>
121
122                   <child>
123                     <widget class="GtkButton" id="BrowserNewButton">
124                       <property name="visible">True</property>
125                       <property name="can_focus">True</property>
126                       <property name="relief">GTK_RELIEF_NONE</property>
127                       <property name="focus_on_click">True</property>
128
129                       <child>
130                         <widget class="GtkImage" id="image303">
131                           <property name="visible">True</property>
132                           <property name="stock">gtk-new</property>
133                           <property name="icon_size">4</property>
134                           <property name="xalign">0.5</property>
135                           <property name="yalign">0.5</property>
136                           <property name="xpad">0</property>
137                           <property name="ypad">0</property>
138                         </widget>
139                       </child>
140                     </widget>
141                     <packing>
142                       <property name="padding">0</property>
143                       <property name="expand">False</property>
144                       <property name="fill">False</property>
145                     </packing>
146                   </child>
147
148                   <child>
149                     <widget class="GtkButton" id="BrowserBackButton">
150                       <property name="visible">True</property>
151                       <property name="can_focus">True</property>
152                       <property name="relief">GTK_RELIEF_NONE</property>
153                       <property name="focus_on_click">True</property>
154
155                       <child>
156                         <widget class="GtkImage" id="image304">
157                           <property name="visible">True</property>
158                           <property name="stock">gtk-go-back</property>
159                           <property name="icon_size">4</property>
160                           <property name="xalign">0.5</property>
161                           <property name="yalign">0.5</property>
162                           <property name="xpad">0</property>
163                           <property name="ypad">0</property>
164                         </widget>
165                       </child>
166                     </widget>
167                     <packing>
168                       <property name="padding">0</property>
169                       <property name="expand">False</property>
170                       <property name="fill">False</property>
171                     </packing>
172                   </child>
173
174                   <child>
175                     <widget class="GtkButton" id="BrowserForwardButton">
176                       <property name="visible">True</property>
177                       <property name="can_focus">True</property>
178                       <property name="relief">GTK_RELIEF_NONE</property>
179                       <property name="focus_on_click">True</property>
180
181                       <child>
182                         <widget class="GtkImage" id="image305">
183                           <property name="visible">True</property>
184                           <property name="stock">gtk-go-forward</property>
185                           <property name="icon_size">4</property>
186                           <property name="xalign">0.5</property>
187                           <property name="yalign">0.5</property>
188                           <property name="xpad">0</property>
189                           <property name="ypad">0</property>
190                         </widget>
191                       </child>
192                     </widget>
193                     <packing>
194                       <property name="padding">0</property>
195                       <property name="expand">False</property>
196                       <property name="fill">False</property>
197                     </packing>
198                   </child>
199
200                   <child>
201                     <widget class="GtkButton" id="BrowserRefreshButton">
202                       <property name="visible">True</property>
203                       <property name="tooltip" translatable="yes">refresh</property>
204                       <property name="can_default">True</property>
205                       <property name="can_focus">True</property>
206                       <property name="relief">GTK_RELIEF_NONE</property>
207                       <property name="focus_on_click">True</property>
208
209                       <child>
210                         <widget class="GtkImage" id="image229">
211                           <property name="visible">True</property>
212                           <property name="stock">gtk-refresh</property>
213                           <property name="icon_size">4</property>
214                           <property name="xalign">0.5</property>
215                           <property name="yalign">0.5</property>
216                           <property name="xpad">0</property>
217                           <property name="ypad">0</property>
218                         </widget>
219                       </child>
220                     </widget>
221                     <packing>
222                       <property name="padding">0</property>
223                       <property name="expand">False</property>
224                       <property name="fill">False</property>
225                     </packing>
226                   </child>
227
228                   <child>
229                     <widget class="GtkButton" id="BrowserHomeButton">
230                       <property name="visible">True</property>
231                       <property name="tooltip" translatable="yes">home</property>
232                       <property name="can_default">True</property>
233                       <property name="can_focus">True</property>
234                       <property name="relief">GTK_RELIEF_NONE</property>
235                       <property name="focus_on_click">True</property>
236
237                       <child>
238                         <widget class="GtkImage" id="image190">
239                           <property name="visible">True</property>
240                           <property name="stock">gtk-home</property>
241                           <property name="icon_size">4</property>
242                           <property name="xalign">0.5</property>
243                           <property name="yalign">0.5</property>
244                           <property name="xpad">0</property>
245                           <property name="ypad">0</property>
246                         </widget>
247                       </child>
248                     </widget>
249                     <packing>
250                       <property name="padding">0</property>
251                       <property name="expand">False</property>
252                       <property name="fill">False</property>
253                     </packing>
254                   </child>
255
256                   <child>
257                     <widget class="GtkImage" id="image301">
258                       <property name="visible">True</property>
259                       <property name="stock">gtk-jump-to</property>
260                       <property name="icon_size">2</property>
261                       <property name="xalign">0.5</property>
262                       <property name="yalign">0.5</property>
263                       <property name="xpad">0</property>
264                       <property name="ypad">0</property>
265                     </widget>
266                     <packing>
267                       <property name="padding">3</property>
268                       <property name="expand">False</property>
269                       <property name="fill">False</property>
270                     </packing>
271                   </child>
272
273                   <child>
274                     <widget class="GtkHBox" id="UriHBox">
275                       <property name="visible">True</property>
276                       <property name="homogeneous">False</property>
277                       <property name="spacing">0</property>
278
279                       <child>
280                         <placeholder/>
281                       </child>
282                     </widget>
283                     <packing>
284                       <property name="padding">0</property>
285                       <property name="expand">True</property>
286                       <property name="fill">True</property>
287                     </packing>
288                   </child>
289                 </widget>
290               </child>
291             </widget>
292             <packing>
293               <property name="padding">0</property>
294               <property name="expand">False</property>
295               <property name="fill">True</property>
296             </packing>
297           </child>
298
299           <child>
300             <widget class="GtkHBox" id="whelpBarBox">
301               <property name="border_width">3</property>
302               <property name="visible">True</property>
303               <property name="homogeneous">False</property>
304               <property name="spacing">6</property>
305
306               <child>
307                 <widget class="GtkImage" id="WhelpBarImage">
308                   <property name="visible">True</property>
309                   <property name="xalign">0.5</property>
310                   <property name="yalign">0.5</property>
311                   <property name="xpad">0</property>
312                   <property name="ypad">0</property>
313                 </widget>
314                 <packing>
315                   <property name="padding">0</property>
316                   <property name="expand">False</property>
317                   <property name="fill">True</property>
318                 </packing>
319               </child>
320
321               <child>
322                 <widget class="GtkEntry" id="queryInputText">
323                   <property name="visible">True</property>
324                   <property name="can_focus">True</property>
325                   <property name="editable">True</property>
326                   <property name="visibility">True</property>
327                   <property name="max_length">0</property>
328                   <property name="text" translatable="yes"></property>
329                   <property name="has_frame">True</property>
330                   <property name="invisible_char">*</property>
331                   <property name="activates_default">False</property>
332                 </widget>
333                 <packing>
334                   <property name="padding">0</property>
335                   <property name="expand">True</property>
336                   <property name="fill">True</property>
337                 </packing>
338               </child>
339
340               <child>
341                 <widget class="GtkVBox" id="whelpBarComboVbox">
342                   <property name="visible">True</property>
343                   <property name="homogeneous">False</property>
344                   <property name="spacing">0</property>
345
346                   <child>
347                     <widget class="GtkAlignment" id="alignment4">
348                       <property name="visible">True</property>
349                       <property name="xalign">0.5</property>
350                       <property name="yalign">0.5</property>
351                       <property name="xscale">1</property>
352                       <property name="yscale">1</property>
353                       <property name="top_padding">0</property>
354                       <property name="bottom_padding">0</property>
355                       <property name="left_padding">0</property>
356                       <property name="right_padding">0</property>
357
358                       <child>
359                         <placeholder/>
360                       </child>
361                     </widget>
362                     <packing>
363                       <property name="padding">0</property>
364                       <property name="expand">False</property>
365                       <property name="fill">False</property>
366                     </packing>
367                   </child>
368                 </widget>
369                 <packing>
370                   <property name="padding">0</property>
371                   <property name="expand">False</property>
372                   <property name="fill">True</property>
373                 </packing>
374               </child>
375             </widget>
376             <packing>
377               <property name="padding">0</property>
378               <property name="expand">False</property>
379               <property name="fill">True</property>
380             </packing>
381           </child>
382
383           <child>
384             <widget class="GtkNotebook" id="mathOrListNotebook">
385               <property name="visible">True</property>
386               <property name="can_focus">True</property>
387               <property name="show_tabs">True</property>
388               <property name="show_border">True</property>
389               <property name="tab_pos">GTK_POS_TOP</property>
390               <property name="scrollable">False</property>
391               <property name="enable_popup">False</property>
392
393               <child>
394                 <widget class="GtkScrolledWindow" id="ScrolledBrowser">
395                   <property name="visible">True</property>
396                   <property name="can_focus">True</property>
397                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
398                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
399                   <property name="shadow_type">GTK_SHADOW_NONE</property>
400                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
401
402                   <child>
403                     <placeholder/>
404                   </child>
405                 </widget>
406                 <packing>
407                   <property name="tab_expand">False</property>
408                   <property name="tab_fill">True</property>
409                 </packing>
410               </child>
411
412               <child>
413                 <widget class="GtkLabel" id="mathLabel">
414                   <property name="visible">True</property>
415                   <property name="label" translatable="yes">MathView</property>
416                   <property name="use_underline">False</property>
417                   <property name="use_markup">False</property>
418                   <property name="justify">GTK_JUSTIFY_LEFT</property>
419                   <property name="wrap">False</property>
420                   <property name="selectable">False</property>
421                   <property name="xalign">0.5</property>
422                   <property name="yalign">0.5</property>
423                   <property name="xpad">0</property>
424                   <property name="ypad">0</property>
425                 </widget>
426                 <packing>
427                   <property name="type">tab</property>
428                 </packing>
429               </child>
430
431               <child>
432                 <widget class="GtkScrolledWindow" id="scrolledwindow9">
433                   <property name="visible">True</property>
434                   <property name="can_focus">True</property>
435                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
436                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
437                   <property name="shadow_type">GTK_SHADOW_IN</property>
438                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
439
440                   <child>
441                     <widget class="GtkTreeView" id="whelpResultTreeview">
442                       <property name="visible">True</property>
443                       <property name="can_focus">True</property>
444                       <property name="headers_visible">False</property>
445                       <property name="rules_hint">False</property>
446                       <property name="reorderable">False</property>
447                       <property name="enable_search">True</property>
448                     </widget>
449                   </child>
450                 </widget>
451                 <packing>
452                   <property name="tab_expand">False</property>
453                   <property name="tab_fill">True</property>
454                 </packing>
455               </child>
456
457               <child>
458                 <widget class="GtkLabel" id="listLabel">
459                   <property name="visible">True</property>
460                   <property name="label" translatable="yes">WhelpResults</property>
461                   <property name="use_underline">False</property>
462                   <property name="use_markup">False</property>
463                   <property name="justify">GTK_JUSTIFY_LEFT</property>
464                   <property name="wrap">False</property>
465                   <property name="selectable">False</property>
466                   <property name="xalign">0.5</property>
467                   <property name="yalign">0.5</property>
468                   <property name="xpad">0</property>
469                   <property name="ypad">0</property>
470                 </widget>
471                 <packing>
472                   <property name="type">tab</property>
473                 </packing>
474               </child>
475             </widget>
476             <packing>
477               <property name="padding">0</property>
478               <property name="expand">True</property>
479               <property name="fill">True</property>
480             </packing>
481           </child>
482         </widget>
483       </child>
484     </widget>
485   </child>
486 </widget>
487
488 <widget class="GtkDialog" id="ConfirmationDialog">
489   <property name="title" translatable="yes">DUMMY</property>
490   <property name="type">GTK_WINDOW_TOPLEVEL</property>
491   <property name="window_position">GTK_WIN_POS_CENTER</property>
492   <property name="modal">True</property>
493   <property name="resizable">False</property>
494   <property name="destroy_with_parent">False</property>
495   <property name="decorated">True</property>
496   <property name="skip_taskbar_hint">False</property>
497   <property name="skip_pager_hint">False</property>
498   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
499   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
500   <property name="has_separator">True</property>
501
502   <child internal-child="vbox">
503     <widget class="GtkVBox" id="dialog-vbox1">
504       <property name="visible">True</property>
505       <property name="homogeneous">False</property>
506       <property name="spacing">0</property>
507
508       <child internal-child="action_area">
509         <widget class="GtkHButtonBox" id="dialog-action_area1">
510           <property name="visible">True</property>
511           <property name="layout_style">GTK_BUTTONBOX_END</property>
512
513           <child>
514             <widget class="GtkButton" id="ConfirmationDialogCancelButton">
515               <property name="visible">True</property>
516               <property name="can_default">True</property>
517               <property name="can_focus">True</property>
518               <property name="label">gtk-cancel</property>
519               <property name="use_stock">True</property>
520               <property name="relief">GTK_RELIEF_NORMAL</property>
521               <property name="focus_on_click">True</property>
522               <property name="response_id">-6</property>
523             </widget>
524           </child>
525
526           <child>
527             <widget class="GtkButton" id="ConfirmationDialogOkButton">
528               <property name="visible">True</property>
529               <property name="can_default">True</property>
530               <property name="can_focus">True</property>
531               <property name="label">gtk-ok</property>
532               <property name="use_stock">True</property>
533               <property name="relief">GTK_RELIEF_NORMAL</property>
534               <property name="focus_on_click">True</property>
535               <property name="response_id">-5</property>
536             </widget>
537           </child>
538         </widget>
539         <packing>
540           <property name="padding">0</property>
541           <property name="expand">False</property>
542           <property name="fill">True</property>
543           <property name="pack_type">GTK_PACK_END</property>
544         </packing>
545       </child>
546
547       <child>
548         <widget class="GtkLabel" id="ConfirmationDialogLabel">
549           <property name="visible">True</property>
550           <property name="label" translatable="yes">DUMMY</property>
551           <property name="use_underline">False</property>
552           <property name="use_markup">False</property>
553           <property name="justify">GTK_JUSTIFY_CENTER</property>
554           <property name="wrap">False</property>
555           <property name="selectable">False</property>
556           <property name="xalign">0.5</property>
557           <property name="yalign">0.5</property>
558           <property name="xpad">0</property>
559           <property name="ypad">0</property>
560         </widget>
561         <packing>
562           <property name="padding">0</property>
563           <property name="expand">False</property>
564           <property name="fill">False</property>
565         </packing>
566       </child>
567     </widget>
568   </child>
569 </widget>
570
571 <widget class="GtkDialog" id="EmptyDialog">
572   <property name="visible">True</property>
573   <property name="title" translatable="yes">DUMMY</property>
574   <property name="type">GTK_WINDOW_TOPLEVEL</property>
575   <property name="window_position">GTK_WIN_POS_NONE</property>
576   <property name="modal">False</property>
577   <property name="resizable">True</property>
578   <property name="destroy_with_parent">False</property>
579   <property name="decorated">True</property>
580   <property name="skip_taskbar_hint">False</property>
581   <property name="skip_pager_hint">False</property>
582   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
583   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
584   <property name="has_separator">True</property>
585
586   <child internal-child="vbox">
587     <widget class="GtkVBox" id="EmptyDialogVBox">
588       <property name="visible">True</property>
589       <property name="homogeneous">False</property>
590       <property name="spacing">0</property>
591
592       <child internal-child="action_area">
593         <widget class="GtkHButtonBox" id="dialog-action_area5">
594           <property name="visible">True</property>
595           <property name="layout_style">GTK_BUTTONBOX_END</property>
596
597           <child>
598             <widget class="GtkButton" id="EmptyDialogCancelButton">
599               <property name="visible">True</property>
600               <property name="can_default">True</property>
601               <property name="can_focus">True</property>
602               <property name="label">gtk-cancel</property>
603               <property name="use_stock">True</property>
604               <property name="relief">GTK_RELIEF_NORMAL</property>
605               <property name="focus_on_click">True</property>
606               <property name="response_id">-6</property>
607             </widget>
608           </child>
609
610           <child>
611             <widget class="GtkButton" id="EmptyDialogOkButton">
612               <property name="visible">True</property>
613               <property name="can_default">True</property>
614               <property name="can_focus">True</property>
615               <property name="label">gtk-ok</property>
616               <property name="use_stock">True</property>
617               <property name="relief">GTK_RELIEF_NORMAL</property>
618               <property name="focus_on_click">True</property>
619               <property name="response_id">-5</property>
620             </widget>
621           </child>
622         </widget>
623         <packing>
624           <property name="padding">0</property>
625           <property name="expand">False</property>
626           <property name="fill">True</property>
627           <property name="pack_type">GTK_PACK_END</property>
628         </packing>
629       </child>
630
631       <child>
632         <widget class="GtkLabel" id="EmptyDialogLabel">
633           <property name="visible">True</property>
634           <property name="label" translatable="yes">DUMMY</property>
635           <property name="use_underline">False</property>
636           <property name="use_markup">False</property>
637           <property name="justify">GTK_JUSTIFY_LEFT</property>
638           <property name="wrap">False</property>
639           <property name="selectable">False</property>
640           <property name="xalign">0.5</property>
641           <property name="yalign">0.5</property>
642           <property name="xpad">0</property>
643           <property name="ypad">0</property>
644         </widget>
645         <packing>
646           <property name="padding">0</property>
647           <property name="expand">False</property>
648           <property name="fill">False</property>
649         </packing>
650       </child>
651
652       <child>
653         <placeholder/>
654       </child>
655     </widget>
656   </child>
657 </widget>
658
659 <widget class="GtkFileSelection" id="FileSelectionWin">
660   <property name="border_width">10</property>
661   <property name="title" translatable="yes">Select File</property>
662   <property name="type">GTK_WINDOW_TOPLEVEL</property>
663   <property name="window_position">GTK_WIN_POS_CENTER</property>
664   <property name="modal">True</property>
665   <property name="resizable">True</property>
666   <property name="destroy_with_parent">False</property>
667   <property name="decorated">True</property>
668   <property name="skip_taskbar_hint">False</property>
669   <property name="skip_pager_hint">False</property>
670   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
671   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
672   <property name="show_fileops">True</property>
673
674   <child internal-child="cancel_button">
675     <widget class="GtkButton" id="fileSelCancelButton">
676       <property name="visible">True</property>
677       <property name="can_default">True</property>
678       <property name="can_focus">True</property>
679       <property name="relief">GTK_RELIEF_NORMAL</property>
680       <property name="focus_on_click">True</property>
681     </widget>
682   </child>
683
684   <child internal-child="ok_button">
685     <widget class="GtkButton" id="fileSelOkButton">
686       <property name="visible">True</property>
687       <property name="can_default">True</property>
688       <property name="can_focus">True</property>
689       <property name="relief">GTK_RELIEF_NORMAL</property>
690       <property name="focus_on_click">True</property>
691     </widget>
692   </child>
693 </widget>
694
695 <widget class="GtkDialog" id="InterpChoiceDialog">
696   <property name="height_request">200</property>
697   <property name="title" translatable="yes">Interpretation choice</property>
698   <property name="type">GTK_WINDOW_TOPLEVEL</property>
699   <property name="window_position">GTK_WIN_POS_NONE</property>
700   <property name="modal">True</property>
701   <property name="resizable">True</property>
702   <property name="destroy_with_parent">False</property>
703   <property name="decorated">True</property>
704   <property name="skip_taskbar_hint">False</property>
705   <property name="skip_pager_hint">False</property>
706   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
707   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
708   <property name="has_separator">True</property>
709
710   <child internal-child="vbox">
711     <widget class="GtkVBox" id="dialog-vbox4">
712       <property name="visible">True</property>
713       <property name="homogeneous">False</property>
714       <property name="spacing">0</property>
715
716       <child internal-child="action_area">
717         <widget class="GtkHButtonBox" id="dialog-action_area4">
718           <property name="visible">True</property>
719           <property name="layout_style">GTK_BUTTONBOX_END</property>
720
721           <child>
722             <widget class="GtkButton" id="InterpChoiceHelpButton">
723               <property name="visible">True</property>
724               <property name="can_default">True</property>
725               <property name="can_focus">True</property>
726               <property name="label">gtk-help</property>
727               <property name="use_stock">True</property>
728               <property name="relief">GTK_RELIEF_NORMAL</property>
729               <property name="focus_on_click">True</property>
730               <property name="response_id">-11</property>
731             </widget>
732           </child>
733
734           <child>
735             <widget class="GtkButton" id="InterpChoiceCancelButton">
736               <property name="visible">True</property>
737               <property name="can_default">True</property>
738               <property name="can_focus">True</property>
739               <property name="label">gtk-cancel</property>
740               <property name="use_stock">True</property>
741               <property name="relief">GTK_RELIEF_NORMAL</property>
742               <property name="focus_on_click">True</property>
743               <property name="response_id">-6</property>
744             </widget>
745           </child>
746
747           <child>
748             <widget class="GtkButton" id="InterpChoiceOkButton">
749               <property name="visible">True</property>
750               <property name="can_default">True</property>
751               <property name="can_focus">True</property>
752               <property name="label">gtk-ok</property>
753               <property name="use_stock">True</property>
754               <property name="relief">GTK_RELIEF_NORMAL</property>
755               <property name="focus_on_click">True</property>
756               <property name="response_id">-5</property>
757             </widget>
758           </child>
759         </widget>
760         <packing>
761           <property name="padding">0</property>
762           <property name="expand">False</property>
763           <property name="fill">True</property>
764           <property name="pack_type">GTK_PACK_END</property>
765         </packing>
766       </child>
767
768       <child>
769         <widget class="GtkVBox" id="vbox3">
770           <property name="visible">True</property>
771           <property name="homogeneous">False</property>
772           <property name="spacing">0</property>
773
774           <child>
775             <widget class="GtkLabel" id="InterpChoiceDialogLabel">
776               <property name="visible">True</property>
777               <property name="label" translatable="yes">some informative message here ...</property>
778               <property name="use_underline">False</property>
779               <property name="use_markup">False</property>
780               <property name="justify">GTK_JUSTIFY_LEFT</property>
781               <property name="wrap">False</property>
782               <property name="selectable">False</property>
783               <property name="xalign">0.5</property>
784               <property name="yalign">0.5</property>
785               <property name="xpad">0</property>
786               <property name="ypad">0</property>
787             </widget>
788             <packing>
789               <property name="padding">0</property>
790               <property name="expand">False</property>
791               <property name="fill">False</property>
792             </packing>
793           </child>
794
795           <child>
796             <widget class="GtkScrolledWindow" id="scrolledwindow4">
797               <property name="visible">True</property>
798               <property name="can_focus">True</property>
799               <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
800               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
801               <property name="shadow_type">GTK_SHADOW_IN</property>
802               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
803
804               <child>
805                 <widget class="GtkTreeView" id="InterpChoiceTreeView">
806                   <property name="visible">True</property>
807                   <property name="can_focus">True</property>
808                   <property name="headers_visible">False</property>
809                   <property name="rules_hint">False</property>
810                   <property name="reorderable">False</property>
811                   <property name="enable_search">True</property>
812                 </widget>
813               </child>
814             </widget>
815             <packing>
816               <property name="padding">0</property>
817               <property name="expand">True</property>
818               <property name="fill">True</property>
819             </packing>
820           </child>
821         </widget>
822         <packing>
823           <property name="padding">0</property>
824           <property name="expand">True</property>
825           <property name="fill">True</property>
826         </packing>
827       </child>
828     </widget>
829   </child>
830 </widget>
831
832 <widget class="GtkWindow" id="MainWin">
833   <property name="title" translatable="yes">Matita</property>
834   <property name="type">GTK_WINDOW_TOPLEVEL</property>
835   <property name="window_position">GTK_WIN_POS_NONE</property>
836   <property name="modal">False</property>
837   <property name="resizable">True</property>
838   <property name="destroy_with_parent">False</property>
839   <property name="decorated">True</property>
840   <property name="skip_taskbar_hint">False</property>
841   <property name="skip_pager_hint">False</property>
842   <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
843   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
844
845   <child>
846     <widget class="GtkEventBox" id="MainWinEventBox">
847       <property name="visible">True</property>
848       <property name="visible_window">True</property>
849       <property name="above_child">False</property>
850
851       <child>
852         <widget class="GtkVBox" id="vbox8">
853           <property name="visible">True</property>
854           <property name="homogeneous">False</property>
855           <property name="spacing">0</property>
856
857           <child>
858             <widget class="GtkHandleBox" id="menuBarHandleBox">
859               <property name="visible">True</property>
860               <property name="shadow_type">GTK_SHADOW_OUT</property>
861               <property name="handle_position">GTK_POS_LEFT</property>
862               <property name="snap_edge">GTK_POS_TOP</property>
863
864               <child>
865                 <widget class="GtkMenuBar" id="menubar1">
866                   <property name="visible">True</property>
867
868                   <child>
869                     <widget class="GtkMenuItem" id="fileMenu">
870                       <property name="visible">True</property>
871                       <property name="label" translatable="yes">_File</property>
872                       <property name="use_underline">True</property>
873
874                       <child>
875                         <widget class="GtkMenu" id="fileMenu_menu">
876
877                           <child>
878                             <widget class="GtkImageMenuItem" id="newMenuItem">
879                               <property name="visible">True</property>
880                               <property name="label" translatable="yes">_New</property>
881                               <property name="use_underline">True</property>
882
883                               <child internal-child="image">
884                                 <widget class="GtkImage" id="image334">
885                                   <property name="visible">True</property>
886                                   <property name="stock">gtk-new</property>
887                                   <property name="icon_size">1</property>
888                                   <property name="xalign">0.5</property>
889                                   <property name="yalign">0.5</property>
890                                   <property name="xpad">0</property>
891                                   <property name="ypad">0</property>
892                                 </widget>
893                               </child>
894                             </widget>
895                           </child>
896
897                           <child>
898                             <widget class="GtkImageMenuItem" id="openMenuItem">
899                               <property name="visible">True</property>
900                               <property name="label" translatable="yes">_Open...</property>
901                               <property name="use_underline">True</property>
902                               <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
903
904                               <child internal-child="image">
905                                 <widget class="GtkImage" id="image335">
906                                   <property name="visible">True</property>
907                                   <property name="stock">gtk-open</property>
908                                   <property name="icon_size">1</property>
909                                   <property name="xalign">0.5</property>
910                                   <property name="yalign">0.5</property>
911                                   <property name="xpad">0</property>
912                                   <property name="ypad">0</property>
913                                 </widget>
914                               </child>
915                             </widget>
916                           </child>
917
918                           <child>
919                             <widget class="GtkImageMenuItem" id="saveMenuItem">
920                               <property name="visible">True</property>
921                               <property name="label" translatable="yes">_Save</property>
922                               <property name="use_underline">True</property>
923                               <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
924
925                               <child internal-child="image">
926                                 <widget class="GtkImage" id="image336">
927                                   <property name="visible">True</property>
928                                   <property name="stock">gtk-save</property>
929                                   <property name="icon_size">1</property>
930                                   <property name="xalign">0.5</property>
931                                   <property name="yalign">0.5</property>
932                                   <property name="xpad">0</property>
933                                   <property name="ypad">0</property>
934                                 </widget>
935                               </child>
936                             </widget>
937                           </child>
938
939                           <child>
940                             <widget class="GtkImageMenuItem" id="saveAsMenuItem">
941                               <property name="visible">True</property>
942                               <property name="label" translatable="yes">Save _As ...</property>
943                               <property name="use_underline">True</property>
944
945                               <child internal-child="image">
946                                 <widget class="GtkImage" id="image337">
947                                   <property name="visible">True</property>
948                                   <property name="stock">gtk-save-as</property>
949                                   <property name="icon_size">1</property>
950                                   <property name="xalign">0.5</property>
951                                   <property name="yalign">0.5</property>
952                                   <property name="xpad">0</property>
953                                   <property name="ypad">0</property>
954                                 </widget>
955                               </child>
956                             </widget>
957                           </child>
958
959                           <child>
960                             <widget class="GtkSeparatorMenuItem" id="separatormenuitem3">
961                               <property name="visible">True</property>
962                             </widget>
963                           </child>
964
965                           <child>
966                             <widget class="GtkImageMenuItem" id="quitMenuItem">
967                               <property name="visible">True</property>
968                               <property name="label" translatable="yes">_Quit</property>
969                               <property name="use_underline">True</property>
970                               <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
971
972                               <child internal-child="image">
973                                 <widget class="GtkImage" id="image338">
974                                   <property name="visible">True</property>
975                                   <property name="stock">gtk-quit</property>
976                                   <property name="icon_size">1</property>
977                                   <property name="xalign">0.5</property>
978                                   <property name="yalign">0.5</property>
979                                   <property name="xpad">0</property>
980                                   <property name="ypad">0</property>
981                                 </widget>
982                               </child>
983                             </widget>
984                           </child>
985                         </widget>
986                       </child>
987                     </widget>
988                   </child>
989
990                   <child>
991                     <widget class="GtkMenuItem" id="editMenu">
992                       <property name="visible">True</property>
993                       <property name="label" translatable="yes">_Edit</property>
994                       <property name="use_underline">True</property>
995                     </widget>
996                   </child>
997
998                   <child>
999                     <widget class="GtkMenuItem" id="viewMenu">
1000                       <property name="visible">True</property>
1001                       <property name="label" translatable="yes">_View</property>
1002                       <property name="use_underline">True</property>
1003
1004                       <child>
1005                         <widget class="GtkMenu" id="viewMenu_menu">
1006
1007                           <child>
1008                             <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
1009                               <property name="visible">True</property>
1010                               <property name="tooltip" translatable="yes">Show/Hide the tactics buttons bar</property>
1011                               <property name="label" translatable="yes">View Tactics Bar</property>
1012                               <property name="use_underline">True</property>
1013                               <property name="active">True</property>
1014                               <accelerator key="F2" modifiers="0" signal="activate"/>
1015                             </widget>
1016                           </child>
1017
1018                           <child>
1019                             <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
1020                               <property name="visible">True</property>
1021                               <property name="label" translatable="yes">New Cic Browser</property>
1022                               <property name="use_underline">True</property>
1023                               <accelerator key="F3" modifiers="0" signal="activate"/>
1024                             </widget>
1025                           </child>
1026
1027                           <child>
1028                             <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
1029                               <property name="visible">True</property>
1030                               <property name="label" translatable="yes">Fullscreen</property>
1031                               <property name="use_underline">True</property>
1032                               <property name="active">False</property>
1033                               <accelerator key="F11" modifiers="0" signal="activate"/>
1034                             </widget>
1035                           </child>
1036
1037                           <child>
1038                             <widget class="GtkSeparatorMenuItem" id="separator1">
1039                               <property name="visible">True</property>
1040                             </widget>
1041                           </child>
1042
1043                           <child>
1044                             <widget class="GtkMenuItem" id="increaseFontSizeMenuItem">
1045                               <property name="visible">True</property>
1046                               <property name="label" translatable="yes">Increase Font Size</property>
1047                               <property name="use_underline">True</property>
1048                               <signal name="activate" handler="on_increaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1049                               <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1050                             </widget>
1051                           </child>
1052
1053                           <child>
1054                             <widget class="GtkMenuItem" id="decreaseFontSizeMenuItem">
1055                               <property name="visible">True</property>
1056                               <property name="label" translatable="yes">Decrease Font Size</property>
1057                               <property name="use_underline">True</property>
1058                               <signal name="activate" handler="on_decreaseFontSizeMenuItem_activate" last_modification_time="Wed, 15 Jun 2005 15:06:29 GMT"/>
1059                               <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1060                             </widget>
1061                           </child>
1062
1063                           <child>
1064                             <widget class="GtkMenuItem" id="normalFontSizeMenuItem">
1065                               <property name="visible">True</property>
1066                               <property name="label" translatable="yes">Normal Font Size</property>
1067                               <property name="use_underline">True</property>
1068                               <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
1069                             </widget>
1070                           </child>
1071                         </widget>
1072                       </child>
1073                     </widget>
1074                   </child>
1075
1076                   <child>
1077                     <widget class="GtkMenuItem" id="debugMenu">
1078                       <property name="visible">True</property>
1079                       <property name="label" translatable="yes">Debug</property>
1080                       <property name="use_underline">True</property>
1081
1082                       <child>
1083                         <widget class="GtkMenu" id="debugMenu_menu">
1084
1085                           <child>
1086                             <widget class="GtkSeparatorMenuItem" id="separatormenuitem5">
1087                               <property name="visible">True</property>
1088                             </widget>
1089                           </child>
1090                         </widget>
1091                       </child>
1092                     </widget>
1093                   </child>
1094
1095                   <child>
1096                     <widget class="GtkMenuItem" id="helpMenu">
1097                       <property name="visible">True</property>
1098                       <property name="label" translatable="yes">_Help</property>
1099                       <property name="use_underline">True</property>
1100
1101                       <child>
1102                         <widget class="GtkMenu" id="helpMenu_menu">
1103
1104                           <child>
1105                             <widget class="GtkMenuItem" id="aboutMenuItem">
1106                               <property name="visible">True</property>
1107                               <property name="label" translatable="yes">About...</property>
1108                               <property name="use_underline">True</property>
1109                             </widget>
1110                           </child>
1111                         </widget>
1112                       </child>
1113                     </widget>
1114                   </child>
1115                 </widget>
1116               </child>
1117             </widget>
1118             <packing>
1119               <property name="padding">0</property>
1120               <property name="expand">False</property>
1121               <property name="fill">False</property>
1122             </packing>
1123           </child>
1124
1125           <child>
1126             <widget class="GtkHBox" id="hbox9">
1127               <property name="visible">True</property>
1128               <property name="homogeneous">False</property>
1129               <property name="spacing">0</property>
1130
1131               <child>
1132                 <widget class="GtkHPaned" id="hpaneScriptSequent">
1133                   <property name="visible">True</property>
1134                   <property name="can_focus">True</property>
1135
1136                   <child>
1137                     <widget class="GtkHBox" id="hbox18">
1138                       <property name="visible">True</property>
1139                       <property name="homogeneous">False</property>
1140                       <property name="spacing">0</property>
1141
1142                       <child>
1143                         <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
1144                           <property name="visible">True</property>
1145                           <property name="shadow_type">GTK_SHADOW_OUT</property>
1146                           <property name="handle_position">GTK_POS_TOP</property>
1147                           <property name="snap_edge">GTK_POS_TOP</property>
1148
1149                           <child>
1150                             <widget class="GtkTable" id="ToolBarTable">
1151                               <property name="visible">True</property>
1152                               <property name="n_rows">17</property>
1153                               <property name="n_columns">2</property>
1154                               <property name="homogeneous">False</property>
1155                               <property name="row_spacing">4</property>
1156                               <property name="column_spacing">0</property>
1157
1158                               <child>
1159                                 <widget class="GtkButton" id="applyButton">
1160                                   <property name="visible">True</property>
1161                                   <property name="tooltip" translatable="yes">Apply</property>
1162                                   <property name="can_focus">True</property>
1163                                   <property name="label" translatable="yes">apply</property>
1164                                   <property name="use_underline">True</property>
1165                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1166                                   <property name="focus_on_click">True</property>
1167                                 </widget>
1168                                 <packing>
1169                                   <property name="left_attach">1</property>
1170                                   <property name="right_attach">2</property>
1171                                   <property name="top_attach">0</property>
1172                                   <property name="bottom_attach">1</property>
1173                                   <property name="x_options">fill</property>
1174                                   <property name="y_options"></property>
1175                                 </packing>
1176                               </child>
1177
1178                               <child>
1179                                 <widget class="GtkButton" id="introsButton">
1180                                   <property name="visible">True</property>
1181                                   <property name="tooltip" translatable="yes">Intros</property>
1182                                   <property name="can_focus">True</property>
1183                                   <property name="label" translatable="yes">intro</property>
1184                                   <property name="use_underline">True</property>
1185                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1186                                   <property name="focus_on_click">True</property>
1187                                 </widget>
1188                                 <packing>
1189                                   <property name="left_attach">0</property>
1190                                   <property name="right_attach">1</property>
1191                                   <property name="top_attach">0</property>
1192                                   <property name="bottom_attach">1</property>
1193                                   <property name="x_options">fill</property>
1194                                   <property name="y_options"></property>
1195                                 </packing>
1196                               </child>
1197
1198                               <child>
1199                                 <widget class="GtkButton" id="exactButton">
1200                                   <property name="visible">True</property>
1201                                   <property name="tooltip" translatable="yes">Exact</property>
1202                                   <property name="can_focus">True</property>
1203                                   <property name="label" translatable="yes">exact</property>
1204                                   <property name="use_underline">True</property>
1205                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1206                                   <property name="focus_on_click">True</property>
1207                                 </widget>
1208                                 <packing>
1209                                   <property name="left_attach">0</property>
1210                                   <property name="right_attach">1</property>
1211                                   <property name="top_attach">2</property>
1212                                   <property name="bottom_attach">3</property>
1213                                   <property name="x_options">fill</property>
1214                                   <property name="y_options"></property>
1215                                 </packing>
1216                               </child>
1217
1218                               <child>
1219                                 <widget class="GtkButton" id="elimButton">
1220                                   <property name="visible">True</property>
1221                                   <property name="tooltip" translatable="yes">Elim</property>
1222                                   <property name="can_focus">True</property>
1223                                   <property name="label" translatable="yes">elim</property>
1224                                   <property name="use_underline">True</property>
1225                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1226                                   <property name="focus_on_click">True</property>
1227                                 </widget>
1228                                 <packing>
1229                                   <property name="left_attach">0</property>
1230                                   <property name="right_attach">1</property>
1231                                   <property name="top_attach">4</property>
1232                                   <property name="bottom_attach">5</property>
1233                                   <property name="x_options">fill</property>
1234                                   <property name="y_options"></property>
1235                                 </packing>
1236                               </child>
1237
1238                               <child>
1239                                 <widget class="GtkButton" id="reflexivityButton">
1240                                   <property name="visible">True</property>
1241                                   <property name="tooltip" translatable="yes">Reflexivity</property>
1242                                   <property name="can_focus">True</property>
1243                                   <property name="label" translatable="yes">refl</property>
1244                                   <property name="use_underline">True</property>
1245                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1246                                   <property name="focus_on_click">True</property>
1247                                 </widget>
1248                                 <packing>
1249                                   <property name="left_attach">0</property>
1250                                   <property name="right_attach">1</property>
1251                                   <property name="top_attach">8</property>
1252                                   <property name="bottom_attach">9</property>
1253                                   <property name="x_options">fill</property>
1254                                   <property name="y_options"></property>
1255                                 </packing>
1256                               </child>
1257
1258                               <child>
1259                                 <widget class="GtkButton" id="symmetryButton">
1260                                   <property name="visible">True</property>
1261                                   <property name="tooltip" translatable="yes">Symmetry</property>
1262                                   <property name="can_focus">True</property>
1263                                   <property name="label" translatable="yes">sym</property>
1264                                   <property name="use_underline">True</property>
1265                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1266                                   <property name="focus_on_click">True</property>
1267                                 </widget>
1268                                 <packing>
1269                                   <property name="left_attach">1</property>
1270                                   <property name="right_attach">2</property>
1271                                   <property name="top_attach">8</property>
1272                                   <property name="bottom_attach">9</property>
1273                                   <property name="x_options">fill</property>
1274                                   <property name="y_options"></property>
1275                                 </packing>
1276                               </child>
1277
1278                               <child>
1279                                 <widget class="GtkButton" id="transitivityButton">
1280                                   <property name="visible">True</property>
1281                                   <property name="tooltip" translatable="yes">Transitivity</property>
1282                                   <property name="can_focus">True</property>
1283                                   <property name="label" translatable="yes">trans</property>
1284                                   <property name="use_underline">True</property>
1285                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1286                                   <property name="focus_on_click">True</property>
1287                                 </widget>
1288                                 <packing>
1289                                   <property name="left_attach">0</property>
1290                                   <property name="right_attach">1</property>
1291                                   <property name="top_attach">9</property>
1292                                   <property name="bottom_attach">10</property>
1293                                   <property name="x_options">fill</property>
1294                                   <property name="y_options"></property>
1295                                 </packing>
1296                               </child>
1297
1298                               <child>
1299                                 <widget class="GtkButton" id="simplifyButton">
1300                                   <property name="visible">True</property>
1301                                   <property name="tooltip" translatable="yes">Simplify</property>
1302                                   <property name="can_focus">True</property>
1303                                   <property name="label" translatable="yes">simpl</property>
1304                                   <property name="use_underline">True</property>
1305                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1306                                   <property name="focus_on_click">True</property>
1307                                 </widget>
1308                                 <packing>
1309                                   <property name="left_attach">0</property>
1310                                   <property name="right_attach">1</property>
1311                                   <property name="top_attach">11</property>
1312                                   <property name="bottom_attach">12</property>
1313                                   <property name="x_options">fill</property>
1314                                   <property name="y_options"></property>
1315                                 </packing>
1316                               </child>
1317
1318                               <child>
1319                                 <widget class="GtkButton" id="reduceButton">
1320                                   <property name="visible">True</property>
1321                                   <property name="tooltip" translatable="yes">Reduce</property>
1322                                   <property name="can_focus">True</property>
1323                                   <property name="label" translatable="yes">red</property>
1324                                   <property name="use_underline">True</property>
1325                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1326                                   <property name="focus_on_click">True</property>
1327                                 </widget>
1328                                 <packing>
1329                                   <property name="left_attach">1</property>
1330                                   <property name="right_attach">2</property>
1331                                   <property name="top_attach">11</property>
1332                                   <property name="bottom_attach">12</property>
1333                                   <property name="x_options">fill</property>
1334                                   <property name="y_options"></property>
1335                                 </packing>
1336                               </child>
1337
1338                               <child>
1339                                 <widget class="GtkButton" id="whdButton">
1340                                   <property name="visible">True</property>
1341                                   <property name="tooltip" translatable="yes">Whd</property>
1342                                   <property name="can_focus">True</property>
1343                                   <property name="label" translatable="yes">whd</property>
1344                                   <property name="use_underline">True</property>
1345                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1346                                   <property name="focus_on_click">True</property>
1347                                 </widget>
1348                                 <packing>
1349                                   <property name="left_attach">0</property>
1350                                   <property name="right_attach">1</property>
1351                                   <property name="top_attach">12</property>
1352                                   <property name="bottom_attach">13</property>
1353                                   <property name="x_options">fill</property>
1354                                   <property name="y_options"></property>
1355                                 </packing>
1356                               </child>
1357
1358                               <child>
1359                                 <widget class="GtkButton" id="assumptionButton">
1360                                   <property name="visible">True</property>
1361                                   <property name="tooltip" translatable="yes">Assumption</property>
1362                                   <property name="can_focus">True</property>
1363                                   <property name="label" translatable="yes">assum</property>
1364                                   <property name="use_underline">True</property>
1365                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1366                                   <property name="focus_on_click">True</property>
1367                                 </widget>
1368                                 <packing>
1369                                   <property name="left_attach">0</property>
1370                                   <property name="right_attach">1</property>
1371                                   <property name="top_attach">14</property>
1372                                   <property name="bottom_attach">15</property>
1373                                   <property name="x_options">fill</property>
1374                                   <property name="y_options"></property>
1375                                 </packing>
1376                               </child>
1377
1378                               <child>
1379                                 <widget class="GtkButton" id="autoButton">
1380                                   <property name="visible">True</property>
1381                                   <property name="tooltip" translatable="yes">Auto</property>
1382                                   <property name="can_focus">True</property>
1383                                   <property name="label" translatable="yes">auto</property>
1384                                   <property name="use_underline">True</property>
1385                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1386                                   <property name="focus_on_click">True</property>
1387                                 </widget>
1388                                 <packing>
1389                                   <property name="left_attach">1</property>
1390                                   <property name="right_attach">2</property>
1391                                   <property name="top_attach">14</property>
1392                                   <property name="bottom_attach">15</property>
1393                                   <property name="x_options">fill</property>
1394                                   <property name="y_options"></property>
1395                                 </packing>
1396                               </child>
1397
1398                               <child>
1399                                 <widget class="GtkButton" id="cutButton">
1400                                   <property name="visible">True</property>
1401                                   <property name="tooltip" translatable="yes">Cut</property>
1402                                   <property name="can_focus">True</property>
1403                                   <property name="label" translatable="yes">cut</property>
1404                                   <property name="use_underline">True</property>
1405                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1406                                   <property name="focus_on_click">True</property>
1407                                 </widget>
1408                                 <packing>
1409                                   <property name="left_attach">0</property>
1410                                   <property name="right_attach">1</property>
1411                                   <property name="top_attach">16</property>
1412                                   <property name="bottom_attach">17</property>
1413                                   <property name="x_options">fill</property>
1414                                   <property name="y_options"></property>
1415                                 </packing>
1416                               </child>
1417
1418                               <child>
1419                                 <widget class="GtkButton" id="replaceButton">
1420                                   <property name="visible">True</property>
1421                                   <property name="tooltip" translatable="yes">Replace</property>
1422                                   <property name="can_focus">True</property>
1423                                   <property name="label" translatable="yes">repl</property>
1424                                   <property name="use_underline">True</property>
1425                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1426                                   <property name="focus_on_click">True</property>
1427                                 </widget>
1428                                 <packing>
1429                                   <property name="left_attach">1</property>
1430                                   <property name="right_attach">2</property>
1431                                   <property name="top_attach">16</property>
1432                                   <property name="bottom_attach">17</property>
1433                                   <property name="x_options">fill</property>
1434                                   <property name="y_options"></property>
1435                                 </packing>
1436                               </child>
1437
1438                               <child>
1439                                 <widget class="GtkButton" id="elimTypeButton">
1440                                   <property name="visible">True</property>
1441                                   <property name="tooltip" translatable="yes">ElimType</property>
1442                                   <property name="can_focus">True</property>
1443                                   <property name="label" translatable="yes">elimTy</property>
1444                                   <property name="use_underline">True</property>
1445                                   <property name="relief">GTK_RELIEF_NORMAL</property>
1446                                   <property name="focus_on_click">True</property>
1447                                 </widget>
1448                                 <packing>
1449                                   <property name="left_attach">1</property>
1450                                   <property name="right_attach">2</property>
1451                                   <property name="top_attach">4</property>
1452                                   <property name="bottom_attach">5</property>
1453                                   <property name="x_options">fill</property>
1454                                   <property name="y_options"></property>
1455                                 </packing>
1456                               </child>
1457
1458                               <child>
1459                                 <widget class="GtkHBox" id="hbox18">
1460                                   <property name="visible">True</property>
1461                                   <property name="homogeneous">True</property>
1462                                   <property name="spacing">0</property>
1463
1464                                   <child>
1465                                     <widget class="GtkButton" id="rightButton">
1466                                       <property name="visible">True</property>
1467                                       <property name="tooltip" translatable="yes">Right</property>
1468                                       <property name="can_focus">True</property>
1469                                       <property name="label" translatable="yes">R</property>
1470                                       <property name="use_underline">True</property>
1471                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1472                                       <property name="focus_on_click">True</property>
1473                                     </widget>
1474                                     <packing>
1475                                       <property name="padding">0</property>
1476                                       <property name="expand">True</property>
1477                                       <property name="fill">True</property>
1478                                     </packing>
1479                                   </child>
1480
1481                                   <child>
1482                                     <widget class="GtkButton" id="existsButton">
1483                                       <property name="visible">True</property>
1484                                       <property name="tooltip" translatable="yes">Exists</property>
1485                                       <property name="can_focus">True</property>
1486                                       <property name="label" translatable="yes">∃</property>
1487                                       <property name="use_underline">True</property>
1488                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1489                                       <property name="focus_on_click">True</property>
1490                                     </widget>
1491                                     <packing>
1492                                       <property name="padding">0</property>
1493                                       <property name="expand">True</property>
1494                                       <property name="fill">True</property>
1495                                     </packing>
1496                                   </child>
1497                                 </widget>
1498                                 <packing>
1499                                   <property name="left_attach">1</property>
1500                                   <property name="right_attach">2</property>
1501                                   <property name="top_attach">6</property>
1502                                   <property name="bottom_attach">7</property>
1503                                   <property name="x_options">fill</property>
1504                                   <property name="y_options">fill</property>
1505                                 </packing>
1506                               </child>
1507
1508                               <child>
1509                                 <widget class="GtkHBox" id="hbox17">
1510                                   <property name="visible">True</property>
1511                                   <property name="homogeneous">True</property>
1512                                   <property name="spacing">0</property>
1513
1514                                   <child>
1515                                     <widget class="GtkButton" id="splitButton">
1516                                       <property name="visible">True</property>
1517                                       <property name="tooltip" translatable="yes">Split</property>
1518                                       <property name="can_focus">True</property>
1519                                       <property name="label" translatable="yes">∧</property>
1520                                       <property name="use_underline">True</property>
1521                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1522                                       <property name="focus_on_click">True</property>
1523                                     </widget>
1524                                     <packing>
1525                                       <property name="padding">0</property>
1526                                       <property name="expand">True</property>
1527                                       <property name="fill">True</property>
1528                                     </packing>
1529                                   </child>
1530
1531                                   <child>
1532                                     <widget class="GtkButton" id="leftButton">
1533                                       <property name="visible">True</property>
1534                                       <property name="tooltip" translatable="yes">Left</property>
1535                                       <property name="can_focus">True</property>
1536                                       <property name="label" translatable="yes">L</property>
1537                                       <property name="use_underline">True</property>
1538                                       <property name="relief">GTK_RELIEF_NORMAL</property>
1539                                       <property name="focus_on_click">True</property>
1540                                     </widget>
1541                                     <packing>
1542                                       <property name="padding">0</property>
1543                                       <property name="expand">True</property>
1544                                       <property name="fill">True</property>
1545                                     </packing>
1546                                   </child>
1547                                 </widget>
1548                                 <packing>
1549                                   <property name="left_attach">0</property>
1550                                   <property name="right_attach">1</property>
1551                                   <property name="top_attach">6</property>
1552                                   <property name="bottom_attach">7</property>
1553                                   <property name="x_options">fill</property>
1554                                   <property name="y_options">fill</property>
1555                                 </packing>
1556                               </child>
1557
1558                               <child>
1559                                 <widget class="GtkAlignment" id="alignment6">
1560                                   <property name="visible">True</property>
1561                                   <property name="xalign">0.5</property>
1562                                   <property name="yalign">0.5</property>
1563                                   <property name="xscale">1</property>
1564                                   <property name="yscale">1</property>
1565                                   <property name="top_padding">0</property>
1566                                   <property name="bottom_padding">0</property>
1567                                   <property name="left_padding">0</property>
1568                                   <property name="right_padding">0</property>
1569
1570                                   <child>
1571                                     <placeholder/>
1572                                   </child>
1573                                 </widget>
1574                                 <packing>
1575                                   <property name="left_attach">0</property>
1576                                   <property name="right_attach">1</property>
1577                                   <property name="top_attach">1</property>
1578                                   <property name="bottom_attach">2</property>
1579                                   <property name="x_options">fill</property>
1580                                 </packing>
1581                               </child>
1582
1583                               <child>
1584                                 <widget class="GtkAlignment" id="alignment7">
1585                                   <property name="visible">True</property>
1586                                   <property name="xalign">0.5</property>
1587                                   <property name="yalign">0.5</property>
1588                                   <property name="xscale">1</property>
1589                                   <property name="yscale">1</property>
1590                                   <property name="top_padding">0</property>
1591                                   <property name="bottom_padding">0</property>
1592                                   <property name="left_padding">0</property>
1593                                   <property name="right_padding">0</property>
1594
1595                                   <child>
1596                                     <placeholder/>
1597                                   </child>
1598                                 </widget>
1599                                 <packing>
1600                                   <property name="left_attach">0</property>
1601                                   <property name="right_attach">1</property>
1602                                   <property name="top_attach">3</property>
1603                                   <property name="bottom_attach">4</property>
1604                                   <property name="x_options">fill</property>
1605                                 </packing>
1606                               </child>
1607
1608                               <child>
1609                                 <widget class="GtkAlignment" id="alignment8">
1610                                   <property name="visible">True</property>
1611                                   <property name="xalign">0.5</property>
1612                                   <property name="yalign">0.5</property>
1613                                   <property name="xscale">1</property>
1614                                   <property name="yscale">1</property>
1615                                   <property name="top_padding">0</property>
1616                                   <property name="bottom_padding">0</property>
1617                                   <property name="left_padding">0</property>
1618                                   <property name="right_padding">0</property>
1619
1620                                   <child>
1621                                     <placeholder/>
1622                                   </child>
1623                                 </widget>
1624                                 <packing>
1625                                   <property name="left_attach">0</property>
1626                                   <property name="right_attach">1</property>
1627                                   <property name="top_attach">5</property>
1628                                   <property name="bottom_attach">6</property>
1629                                   <property name="x_options">fill</property>
1630                                 </packing>
1631                               </child>
1632
1633                               <child>
1634                                 <widget class="GtkAlignment" id="alignment9">
1635                                   <property name="visible">True</property>
1636                                   <property name="xalign">0.5</property>
1637                                   <property name="yalign">0.5</property>
1638                                   <property name="xscale">1</property>
1639                                   <property name="yscale">1</property>
1640                                   <property name="top_padding">0</property>
1641                                   <property name="bottom_padding">0</property>
1642                                   <property name="left_padding">0</property>
1643                                   <property name="right_padding">0</property>
1644
1645                                   <child>
1646                                     <placeholder/>
1647                                   </child>
1648                                 </widget>
1649                                 <packing>
1650                                   <property name="left_attach">0</property>
1651                                   <property name="right_attach">1</property>
1652                                   <property name="top_attach">7</property>
1653                                   <property name="bottom_attach">8</property>
1654                                   <property name="x_options">fill</property>
1655                                 </packing>
1656                               </child>
1657
1658                               <child>
1659                                 <widget class="GtkAlignment" id="alignment10">
1660                                   <property name="visible">True</property>
1661                                   <property name="xalign">0.5</property>
1662                                   <property name="yalign">0.5</property>
1663                                   <property name="xscale">1</property>
1664                                   <property name="yscale">1</property>
1665                                   <property name="top_padding">0</property>
1666                                   <property name="bottom_padding">0</property>
1667                                   <property name="left_padding">0</property>
1668                                   <property name="right_padding">0</property>
1669
1670                                   <child>
1671                                     <placeholder/>
1672                                   </child>
1673                                 </widget>
1674                                 <packing>
1675                                   <property name="left_attach">0</property>
1676                                   <property name="right_attach">1</property>
1677                                   <property name="top_attach">10</property>
1678                                   <property name="bottom_attach">11</property>
1679                                   <property name="x_options">fill</property>
1680                                 </packing>
1681                               </child>
1682
1683                               <child>
1684                                 <widget class="GtkAlignment" id="alignment11">
1685                                   <property name="visible">True</property>
1686                                   <property name="xalign">0.5</property>
1687                                   <property name="yalign">0.5</property>
1688                                   <property name="xscale">1</property>
1689                                   <property name="yscale">1</property>
1690                                   <property name="top_padding">0</property>
1691                                   <property name="bottom_padding">0</property>
1692                                   <property name="left_padding">0</property>
1693                                   <property name="right_padding">0</property>
1694
1695                                   <child>
1696                                     <placeholder/>
1697                                   </child>
1698                                 </widget>
1699                                 <packing>
1700                                   <property name="left_attach">0</property>
1701                                   <property name="right_attach">1</property>
1702                                   <property name="top_attach">13</property>
1703                                   <property name="bottom_attach">14</property>
1704                                   <property name="x_options">fill</property>
1705                                 </packing>
1706                               </child>
1707
1708                               <child>
1709                                 <widget class="GtkAlignment" id="alignment12">
1710                                   <property name="visible">True</property>
1711                                   <property name="xalign">0.5</property>
1712                                   <property name="yalign">0.5</property>
1713                                   <property name="xscale">1</property>
1714                                   <property name="yscale">1</property>
1715                                   <property name="top_padding">0</property>
1716                                   <property name="bottom_padding">0</property>
1717                                   <property name="left_padding">0</property>
1718                                   <property name="right_padding">0</property>
1719
1720                                   <child>
1721                                     <placeholder/>
1722                                   </child>
1723                                 </widget>
1724                                 <packing>
1725                                   <property name="left_attach">0</property>
1726                                   <property name="right_attach">1</property>
1727                                   <property name="top_attach">15</property>
1728                                   <property name="bottom_attach">16</property>
1729                                   <property name="x_options">fill</property>
1730                                 </packing>
1731                               </child>
1732                             </widget>
1733                           </child>
1734                         </widget>
1735                         <packing>
1736                           <property name="padding">0</property>
1737                           <property name="expand">False</property>
1738                           <property name="fill">True</property>
1739                         </packing>
1740                       </child>
1741
1742                       <child>
1743                         <widget class="GtkVBox" id="vboxScript">
1744                           <property name="width_request">400</property>
1745                           <property name="visible">True</property>
1746                           <property name="homogeneous">False</property>
1747                           <property name="spacing">0</property>
1748
1749                           <child>
1750                             <widget class="GtkToolbar" id="toolbar13">
1751                               <property name="visible">True</property>
1752                               <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
1753                               <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
1754                               <property name="tooltips">True</property>
1755                               <property name="show_arrow">True</property>
1756
1757                               <child>
1758                                 <widget class="GtkToolItem" id="toolitem25">
1759                                   <property name="visible">True</property>
1760                                   <property name="visible_horizontal">True</property>
1761                                   <property name="visible_vertical">True</property>
1762                                   <property name="is_important">False</property>
1763
1764                                   <child>
1765                                     <widget class="GtkButton" id="scriptTopButton">
1766                                       <property name="visible">True</property>
1767                                       <property name="tooltip" translatable="yes">restart (Home)</property>
1768                                       <property name="can_focus">True</property>
1769                                       <property name="relief">GTK_RELIEF_NONE</property>
1770                                       <property name="focus_on_click">True</property>
1771                                       <accelerator key="Home" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
1772
1773                                       <child>
1774                                         <widget class="GtkImage" id="image253">
1775                                           <property name="visible">True</property>
1776                                           <property name="stock">gtk-goto-top</property>
1777                                           <property name="icon_size">4</property>
1778                                           <property name="xalign">0.5</property>
1779                                           <property name="yalign">0.5</property>
1780                                           <property name="xpad">0</property>
1781                                           <property name="ypad">0</property>
1782                                         </widget>
1783                                       </child>
1784                                     </widget>
1785                                   </child>
1786                                 </widget>
1787                                 <packing>
1788                                   <property name="expand">False</property>
1789                                   <property name="homogeneous">False</property>
1790                                 </packing>
1791                               </child>
1792
1793                               <child>
1794                                 <widget class="GtkToolItem" id="toolitem26">
1795                                   <property name="visible">True</property>
1796                                   <property name="visible_horizontal">True</property>
1797                                   <property name="visible_vertical">True</property>
1798                                   <property name="is_important">False</property>
1799
1800                                   <child>
1801                                     <widget class="GtkButton" id="scriptRetractButton">
1802                                       <property name="visible">True</property>
1803                                       <property name="tooltip" translatable="yes">go back 1 phrase (Page Up)</property>
1804                                       <property name="can_focus">True</property>
1805                                       <property name="relief">GTK_RELIEF_NONE</property>
1806                                       <property name="focus_on_click">True</property>
1807                                       <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
1808
1809                                       <child>
1810                                         <widget class="GtkImage" id="image254">
1811                                           <property name="visible">True</property>
1812                                           <property name="stock">gtk-go-up</property>
1813                                           <property name="icon_size">4</property>
1814                                           <property name="xalign">0.5</property>
1815                                           <property name="yalign">0.5</property>
1816                                           <property name="xpad">0</property>
1817                                           <property name="ypad">0</property>
1818                                         </widget>
1819                                       </child>
1820                                     </widget>
1821                                   </child>
1822                                 </widget>
1823                                 <packing>
1824                                   <property name="expand">False</property>
1825                                   <property name="homogeneous">False</property>
1826                                 </packing>
1827                               </child>
1828
1829                               <child>
1830                                 <widget class="GtkToolItem" id="toolitem27">
1831                                   <property name="visible">True</property>
1832                                   <property name="visible_horizontal">True</property>
1833                                   <property name="visible_vertical">True</property>
1834                                   <property name="is_important">False</property>
1835
1836                                   <child>
1837                                     <widget class="GtkButton" id="scriptJumpButton">
1838                                       <property name="visible">True</property>
1839                                       <property name="tooltip" translatable="yes">execute until point</property>
1840                                       <property name="can_focus">True</property>
1841                                       <property name="relief">GTK_RELIEF_NONE</property>
1842                                       <property name="focus_on_click">True</property>
1843
1844                                       <child>
1845                                         <widget class="GtkImage" id="image255">
1846                                           <property name="visible">True</property>
1847                                           <property name="stock">gtk-jump-to</property>
1848                                           <property name="icon_size">4</property>
1849                                           <property name="xalign">0.5</property>
1850                                           <property name="yalign">0.5</property>
1851                                           <property name="xpad">0</property>
1852                                           <property name="ypad">0</property>
1853                                         </widget>
1854                                       </child>
1855                                     </widget>
1856                                   </child>
1857                                 </widget>
1858                                 <packing>
1859                                   <property name="expand">False</property>
1860                                   <property name="homogeneous">False</property>
1861                                 </packing>
1862                               </child>
1863
1864                               <child>
1865                                 <widget class="GtkToolItem" id="toolitem28">
1866                                   <property name="visible">True</property>
1867                                   <property name="visible_horizontal">True</property>
1868                                   <property name="visible_vertical">True</property>
1869                                   <property name="is_important">False</property>
1870
1871                                   <child>
1872                                     <widget class="GtkButton" id="scriptAdvanceButton">
1873                                       <property name="visible">True</property>
1874                                       <property name="tooltip" translatable="yes">go forward 1 phrase (Page Down)</property>
1875                                       <property name="can_focus">True</property>
1876                                       <property name="relief">GTK_RELIEF_NONE</property>
1877                                       <property name="focus_on_click">True</property>
1878                                       <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
1879
1880                                       <child>
1881                                         <widget class="GtkImage" id="image256">
1882                                           <property name="visible">True</property>
1883                                           <property name="stock">gtk-go-down</property>
1884                                           <property name="icon_size">4</property>
1885                                           <property name="xalign">0.5</property>
1886                                           <property name="yalign">0.5</property>
1887                                           <property name="xpad">0</property>
1888                                           <property name="ypad">0</property>
1889                                         </widget>
1890                                       </child>
1891                                     </widget>
1892                                   </child>
1893                                 </widget>
1894                                 <packing>
1895                                   <property name="expand">False</property>
1896                                   <property name="homogeneous">False</property>
1897                                 </packing>
1898                               </child>
1899
1900                               <child>
1901                                 <widget class="GtkToolItem" id="toolitem29">
1902                                   <property name="visible">True</property>
1903                                   <property name="visible_horizontal">True</property>
1904                                   <property name="visible_vertical">True</property>
1905                                   <property name="is_important">False</property>
1906
1907                                   <child>
1908                                     <widget class="GtkButton" id="scriptBottomButton">
1909                                       <property name="visible">True</property>
1910                                       <property name="tooltip" translatable="yes">execute all (End)</property>
1911                                       <property name="can_focus">True</property>
1912                                       <property name="relief">GTK_RELIEF_NONE</property>
1913                                       <property name="focus_on_click">True</property>
1914                                       <accelerator key="End" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
1915
1916                                       <child>
1917                                         <widget class="GtkImage" id="image257">
1918                                           <property name="visible">True</property>
1919                                           <property name="stock">gtk-goto-bottom</property>
1920                                           <property name="icon_size">4</property>
1921                                           <property name="xalign">0.5</property>
1922                                           <property name="yalign">0.5</property>
1923                                           <property name="xpad">0</property>
1924                                           <property name="ypad">0</property>
1925                                         </widget>
1926                                       </child>
1927                                     </widget>
1928                                   </child>
1929                                 </widget>
1930                                 <packing>
1931                                   <property name="expand">False</property>
1932                                   <property name="homogeneous">False</property>
1933                                 </packing>
1934                               </child>
1935                             </widget>
1936                             <packing>
1937                               <property name="padding">0</property>
1938                               <property name="expand">False</property>
1939                               <property name="fill">False</property>
1940                             </packing>
1941                           </child>
1942
1943                           <child>
1944                             <widget class="GtkNotebook" id="scriptNotebook">
1945                               <property name="visible">True</property>
1946                               <property name="can_focus">True</property>
1947                               <property name="show_tabs">True</property>
1948                               <property name="show_border">True</property>
1949                               <property name="tab_pos">GTK_POS_BOTTOM</property>
1950                               <property name="scrollable">False</property>
1951                               <property name="enable_popup">False</property>
1952
1953                               <child>
1954                                 <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
1955                                   <property name="visible">True</property>
1956                                   <property name="can_focus">True</property>
1957                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1958                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1959                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
1960                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1961
1962                                   <child>
1963                                     <placeholder/>
1964                                   </child>
1965                                 </widget>
1966                                 <packing>
1967                                   <property name="tab_expand">False</property>
1968                                   <property name="tab_fill">True</property>
1969                                 </packing>
1970                               </child>
1971
1972                               <child>
1973                                 <widget class="GtkLabel" id="scriptLabel">
1974                                   <property name="visible">True</property>
1975                                   <property name="label" translatable="yes">script</property>
1976                                   <property name="use_underline">False</property>
1977                                   <property name="use_markup">False</property>
1978                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
1979                                   <property name="wrap">False</property>
1980                                   <property name="selectable">False</property>
1981                                   <property name="xalign">0.5</property>
1982                                   <property name="yalign">0.5</property>
1983                                   <property name="xpad">0</property>
1984                                   <property name="ypad">0</property>
1985                                 </widget>
1986                                 <packing>
1987                                   <property name="type">tab</property>
1988                                 </packing>
1989                               </child>
1990
1991                               <child>
1992                                 <widget class="GtkScrolledWindow" id="scrolledwindow8">
1993                                   <property name="visible">True</property>
1994                                   <property name="can_focus">True</property>
1995                                   <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1996                                   <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
1997                                   <property name="shadow_type">GTK_SHADOW_NONE</property>
1998                                   <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
1999
2000                                   <child>
2001                                     <widget class="GtkTreeView" id="scriptTreeView">
2002                                       <property name="visible">True</property>
2003                                       <property name="can_focus">True</property>
2004                                       <property name="headers_visible">False</property>
2005                                       <property name="rules_hint">False</property>
2006                                       <property name="reorderable">False</property>
2007                                       <property name="enable_search">True</property>
2008                                     </widget>
2009                                   </child>
2010                                 </widget>
2011                                 <packing>
2012                                   <property name="tab_expand">False</property>
2013                                   <property name="tab_fill">True</property>
2014                                 </packing>
2015                               </child>
2016
2017                               <child>
2018                                 <widget class="GtkLabel" id="label13">
2019                                   <property name="visible">True</property>
2020                                   <property name="label" translatable="yes">outline</property>
2021                                   <property name="use_underline">False</property>
2022                                   <property name="use_markup">False</property>
2023                                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2024                                   <property name="wrap">False</property>
2025                                   <property name="selectable">False</property>
2026                                   <property name="xalign">0.5</property>
2027                                   <property name="yalign">0.5</property>
2028                                   <property name="xpad">0</property>
2029                                   <property name="ypad">0</property>
2030                                 </widget>
2031                                 <packing>
2032                                   <property name="type">tab</property>
2033                                 </packing>
2034                               </child>
2035                             </widget>
2036                             <packing>
2037                               <property name="padding">0</property>
2038                               <property name="expand">True</property>
2039                               <property name="fill">True</property>
2040                             </packing>
2041                           </child>
2042                         </widget>
2043                         <packing>
2044                           <property name="padding">0</property>
2045                           <property name="expand">True</property>
2046                           <property name="fill">True</property>
2047                         </packing>
2048                       </child>
2049                     </widget>
2050                     <packing>
2051                       <property name="shrink">True</property>
2052                       <property name="resize">False</property>
2053                     </packing>
2054                   </child>
2055
2056                   <child>
2057                     <widget class="GtkVPaned" id="vpaned1">
2058                       <property name="width_request">250</property>
2059                       <property name="height_request">500</property>
2060                       <property name="visible">True</property>
2061                       <property name="can_focus">True</property>
2062                       <property name="position">380</property>
2063
2064                       <child>
2065                         <widget class="GtkNotebook" id="sequentsNotebook">
2066                           <property name="visible">True</property>
2067                           <property name="can_focus">True</property>
2068                           <property name="show_tabs">True</property>
2069                           <property name="show_border">True</property>
2070                           <property name="tab_pos">GTK_POS_TOP</property>
2071                           <property name="scrollable">False</property>
2072                           <property name="enable_popup">False</property>
2073                         </widget>
2074                         <packing>
2075                           <property name="shrink">True</property>
2076                           <property name="resize">False</property>
2077                         </packing>
2078                       </child>
2079
2080                       <child>
2081                         <widget class="GtkHBox" id="hbox9">
2082                           <property name="visible">True</property>
2083                           <property name="homogeneous">False</property>
2084                           <property name="spacing">0</property>
2085
2086                           <child>
2087                             <widget class="GtkScrolledWindow" id="logScrolledWin">
2088                               <property name="visible">True</property>
2089                               <property name="can_focus">True</property>
2090                               <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
2091                               <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
2092                               <property name="shadow_type">GTK_SHADOW_IN</property>
2093                               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2094
2095                               <child>
2096                                 <widget class="GtkTextView" id="logTextView">
2097                                   <property name="visible">True</property>
2098                                   <property name="can_focus">True</property>
2099                                   <property name="editable">False</property>
2100                                   <property name="overwrite">False</property>
2101                                   <property name="accepts_tab">True</property>
2102                                   <property name="justification">GTK_JUSTIFY_LEFT</property>
2103                                   <property name="wrap_mode">GTK_WRAP_CHAR</property>
2104                                   <property name="cursor_visible">False</property>
2105                                   <property name="pixels_above_lines">0</property>
2106                                   <property name="pixels_below_lines">0</property>
2107                                   <property name="pixels_inside_wrap">0</property>
2108                                   <property name="left_margin">0</property>
2109                                   <property name="right_margin">0</property>
2110                                   <property name="indent">0</property>
2111                                   <property name="text" translatable="yes"></property>
2112                                 </widget>
2113                               </child>
2114                             </widget>
2115                             <packing>
2116                               <property name="padding">0</property>
2117                               <property name="expand">True</property>
2118                               <property name="fill">True</property>
2119                             </packing>
2120                           </child>
2121                         </widget>
2122                         <packing>
2123                           <property name="shrink">True</property>
2124                           <property name="resize">True</property>
2125                         </packing>
2126                       </child>
2127                     </widget>
2128                     <packing>
2129                       <property name="shrink">True</property>
2130                       <property name="resize">True</property>
2131                     </packing>
2132                   </child>
2133                 </widget>
2134                 <packing>
2135                   <property name="padding">0</property>
2136                   <property name="expand">True</property>
2137                   <property name="fill">True</property>
2138                 </packing>
2139               </child>
2140             </widget>
2141             <packing>
2142               <property name="padding">0</property>
2143               <property name="expand">True</property>
2144               <property name="fill">True</property>
2145             </packing>
2146           </child>
2147
2148           <child>
2149             <widget class="GtkHBox" id="hbox10">
2150               <property name="visible">True</property>
2151               <property name="homogeneous">False</property>
2152               <property name="spacing">0</property>
2153
2154               <child>
2155                 <widget class="GtkStatusbar" id="StatusBar">
2156                   <property name="visible">True</property>
2157                   <property name="has_resize_grip">False</property>
2158                 </widget>
2159                 <packing>
2160                   <property name="padding">0</property>
2161                   <property name="expand">True</property>
2162                   <property name="fill">True</property>
2163                 </packing>
2164               </child>
2165
2166               <child>
2167                 <widget class="GtkNotebook" id="HintNotebook">
2168                   <property name="visible">True</property>
2169                   <property name="show_tabs">False</property>
2170                   <property name="show_border">True</property>
2171                   <property name="tab_pos">GTK_POS_TOP</property>
2172                   <property name="scrollable">False</property>
2173                   <property name="enable_popup">False</property>
2174
2175                   <child>
2176                     <widget class="GtkImage" id="HintLowImage">
2177                       <property name="visible">True</property>
2178                       <property name="xalign">0.5</property>
2179                       <property name="yalign">0.5</property>
2180                       <property name="xpad">0</property>
2181                       <property name="ypad">0</property>
2182                     </widget>
2183                     <packing>
2184                       <property name="tab_expand">False</property>
2185                       <property name="tab_fill">True</property>
2186                     </packing>
2187                   </child>
2188
2189                   <child>
2190                     <widget class="GtkLabel" id="label14">
2191                       <property name="visible">True</property>
2192                       <property name="label" translatable="yes">label14</property>
2193                       <property name="use_underline">False</property>
2194                       <property name="use_markup">False</property>
2195                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2196                       <property name="wrap">False</property>
2197                       <property name="selectable">False</property>
2198                       <property name="xalign">0.5</property>
2199                       <property name="yalign">0.5</property>
2200                       <property name="xpad">0</property>
2201                       <property name="ypad">0</property>
2202                     </widget>
2203                     <packing>
2204                       <property name="type">tab</property>
2205                     </packing>
2206                   </child>
2207
2208                   <child>
2209                     <widget class="GtkImage" id="HintMediumImage">
2210                       <property name="visible">True</property>
2211                       <property name="xalign">0.5</property>
2212                       <property name="yalign">0.5</property>
2213                       <property name="xpad">0</property>
2214                       <property name="ypad">0</property>
2215                     </widget>
2216                     <packing>
2217                       <property name="tab_expand">False</property>
2218                       <property name="tab_fill">True</property>
2219                     </packing>
2220                   </child>
2221
2222                   <child>
2223                     <widget class="GtkLabel" id="label15">
2224                       <property name="visible">True</property>
2225                       <property name="label" translatable="yes">label15</property>
2226                       <property name="use_underline">False</property>
2227                       <property name="use_markup">False</property>
2228                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2229                       <property name="wrap">False</property>
2230                       <property name="selectable">False</property>
2231                       <property name="xalign">0.5</property>
2232                       <property name="yalign">0.5</property>
2233                       <property name="xpad">0</property>
2234                       <property name="ypad">0</property>
2235                     </widget>
2236                     <packing>
2237                       <property name="type">tab</property>
2238                     </packing>
2239                   </child>
2240
2241                   <child>
2242                     <widget class="GtkImage" id="HintHighImage">
2243                       <property name="visible">True</property>
2244                       <property name="xalign">0.5</property>
2245                       <property name="yalign">0.5</property>
2246                       <property name="xpad">0</property>
2247                       <property name="ypad">0</property>
2248                     </widget>
2249                     <packing>
2250                       <property name="tab_expand">False</property>
2251                       <property name="tab_fill">True</property>
2252                     </packing>
2253                   </child>
2254
2255                   <child>
2256                     <widget class="GtkLabel" id="label16">
2257                       <property name="visible">True</property>
2258                       <property name="label" translatable="yes">label16</property>
2259                       <property name="use_underline">False</property>
2260                       <property name="use_markup">False</property>
2261                       <property name="justify">GTK_JUSTIFY_LEFT</property>
2262                       <property name="wrap">False</property>
2263                       <property name="selectable">False</property>
2264                       <property name="xalign">0.5</property>
2265                       <property name="yalign">0.5</property>
2266                       <property name="xpad">0</property>
2267                       <property name="ypad">0</property>
2268                     </widget>
2269                     <packing>
2270                       <property name="type">tab</property>
2271                     </packing>
2272                   </child>
2273                 </widget>
2274                 <packing>
2275                   <property name="padding">0</property>
2276                   <property name="expand">False</property>
2277                   <property name="fill">True</property>
2278                 </packing>
2279               </child>
2280             </widget>
2281             <packing>
2282               <property name="padding">0</property>
2283               <property name="expand">False</property>
2284               <property name="fill">False</property>
2285             </packing>
2286           </child>
2287         </widget>
2288       </child>
2289     </widget>
2290   </child>
2291 </widget>
2292
2293 <widget class="GtkDialog" id="TextDialog">
2294   <property name="title" translatable="yes">DUMMY</property>
2295   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2296   <property name="window_position">GTK_WIN_POS_NONE</property>
2297   <property name="modal">False</property>
2298   <property name="resizable">True</property>
2299   <property name="destroy_with_parent">False</property>
2300   <property name="decorated">True</property>
2301   <property name="skip_taskbar_hint">False</property>
2302   <property name="skip_pager_hint">False</property>
2303   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2304   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2305   <property name="has_separator">True</property>
2306
2307   <child internal-child="vbox">
2308     <widget class="GtkVBox" id="vbox5">
2309       <property name="visible">True</property>
2310       <property name="homogeneous">False</property>
2311       <property name="spacing">0</property>
2312
2313       <child internal-child="action_area">
2314         <widget class="GtkHButtonBox" id="hbuttonbox1">
2315           <property name="visible">True</property>
2316           <property name="layout_style">GTK_BUTTONBOX_END</property>
2317
2318           <child>
2319             <widget class="GtkButton" id="TextDialogCancelButton">
2320               <property name="visible">True</property>
2321               <property name="can_default">True</property>
2322               <property name="can_focus">True</property>
2323               <property name="label">gtk-cancel</property>
2324               <property name="use_stock">True</property>
2325               <property name="relief">GTK_RELIEF_NORMAL</property>
2326               <property name="focus_on_click">True</property>
2327               <property name="response_id">-6</property>
2328             </widget>
2329           </child>
2330
2331           <child>
2332             <widget class="GtkButton" id="TextDialogOkButton">
2333               <property name="visible">True</property>
2334               <property name="can_default">True</property>
2335               <property name="can_focus">True</property>
2336               <property name="label">gtk-ok</property>
2337               <property name="use_stock">True</property>
2338               <property name="relief">GTK_RELIEF_NORMAL</property>
2339               <property name="focus_on_click">True</property>
2340               <property name="response_id">-5</property>
2341             </widget>
2342           </child>
2343         </widget>
2344         <packing>
2345           <property name="padding">0</property>
2346           <property name="expand">False</property>
2347           <property name="fill">True</property>
2348           <property name="pack_type">GTK_PACK_END</property>
2349         </packing>
2350       </child>
2351
2352       <child>
2353         <widget class="GtkLabel" id="TextDialogLabel">
2354           <property name="visible">True</property>
2355           <property name="label" translatable="yes">DUMMY</property>
2356           <property name="use_underline">False</property>
2357           <property name="use_markup">False</property>
2358           <property name="justify">GTK_JUSTIFY_LEFT</property>
2359           <property name="wrap">False</property>
2360           <property name="selectable">False</property>
2361           <property name="xalign">0.5</property>
2362           <property name="yalign">0.5</property>
2363           <property name="xpad">0</property>
2364           <property name="ypad">0</property>
2365         </widget>
2366         <packing>
2367           <property name="padding">0</property>
2368           <property name="expand">False</property>
2369           <property name="fill">False</property>
2370         </packing>
2371       </child>
2372
2373       <child>
2374         <widget class="GtkScrolledWindow" id="scrolledwindow2">
2375           <property name="visible">True</property>
2376           <property name="can_focus">True</property>
2377           <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2378           <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2379           <property name="shadow_type">GTK_SHADOW_IN</property>
2380           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2381
2382           <child>
2383             <widget class="GtkTextView" id="TextDialogTextView">
2384               <property name="visible">True</property>
2385               <property name="can_focus">True</property>
2386               <property name="editable">True</property>
2387               <property name="overwrite">False</property>
2388               <property name="accepts_tab">True</property>
2389               <property name="justification">GTK_JUSTIFY_LEFT</property>
2390               <property name="wrap_mode">GTK_WRAP_NONE</property>
2391               <property name="cursor_visible">True</property>
2392               <property name="pixels_above_lines">0</property>
2393               <property name="pixels_below_lines">0</property>
2394               <property name="pixels_inside_wrap">0</property>
2395               <property name="left_margin">0</property>
2396               <property name="right_margin">0</property>
2397               <property name="indent">0</property>
2398               <property name="text" translatable="yes"></property>
2399             </widget>
2400           </child>
2401         </widget>
2402         <packing>
2403           <property name="padding">0</property>
2404           <property name="expand">True</property>
2405           <property name="fill">True</property>
2406         </packing>
2407       </child>
2408     </widget>
2409   </child>
2410 </widget>
2411
2412 <widget class="GtkDialog" id="UriChoiceDialog">
2413   <property name="height_request">280</property>
2414   <property name="title" translatable="yes">Uri choice</property>
2415   <property name="type">GTK_WINDOW_TOPLEVEL</property>
2416   <property name="window_position">GTK_WIN_POS_CENTER</property>
2417   <property name="modal">True</property>
2418   <property name="resizable">True</property>
2419   <property name="destroy_with_parent">False</property>
2420   <property name="decorated">True</property>
2421   <property name="skip_taskbar_hint">False</property>
2422   <property name="skip_pager_hint">False</property>
2423   <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
2424   <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
2425   <property name="has_separator">True</property>
2426
2427   <child internal-child="vbox">
2428     <widget class="GtkVBox" id="dialog-vbox3">
2429       <property name="visible">True</property>
2430       <property name="homogeneous">False</property>
2431       <property name="spacing">4</property>
2432
2433       <child internal-child="action_area">
2434         <widget class="GtkHButtonBox" id="dialog-action_area3">
2435           <property name="visible">True</property>
2436           <property name="layout_style">GTK_BUTTONBOX_END</property>
2437
2438           <child>
2439             <widget class="GtkButton" id="UriChoiceAbortButton">
2440               <property name="visible">True</property>
2441               <property name="can_default">True</property>
2442               <property name="can_focus">True</property>
2443               <property name="label">gtk-cancel</property>
2444               <property name="use_stock">True</property>
2445               <property name="relief">GTK_RELIEF_NORMAL</property>
2446               <property name="focus_on_click">True</property>
2447               <property name="response_id">-6</property>
2448             </widget>
2449           </child>
2450
2451           <child>
2452             <widget class="GtkButton" id="UriChoiceSelectedButton">
2453               <property name="visible">True</property>
2454               <property name="can_default">True</property>
2455               <property name="can_focus">True</property>
2456               <property name="relief">GTK_RELIEF_NORMAL</property>
2457               <property name="focus_on_click">True</property>
2458               <property name="response_id">0</property>
2459
2460               <child>
2461                 <widget class="GtkAlignment" id="alignment2">
2462                   <property name="visible">True</property>
2463                   <property name="xalign">0.5</property>
2464                   <property name="yalign">0.5</property>
2465                   <property name="xscale">0</property>
2466                   <property name="yscale">0</property>
2467                   <property name="top_padding">0</property>
2468                   <property name="bottom_padding">0</property>
2469                   <property name="left_padding">0</property>
2470                   <property name="right_padding">0</property>
2471
2472                   <child>
2473                     <widget class="GtkHBox" id="hbox3">
2474                       <property name="visible">True</property>
2475                       <property name="homogeneous">False</property>
2476                       <property name="spacing">2</property>
2477
2478                       <child>
2479                         <widget class="GtkImage" id="image19">
2480                           <property name="visible">True</property>
2481                           <property name="stock">gtk-index</property>
2482                           <property name="icon_size">4</property>
2483                           <property name="xalign">0.5</property>
2484                           <property name="yalign">0.5</property>
2485                           <property name="xpad">0</property>
2486                           <property name="ypad">0</property>
2487                         </widget>
2488                         <packing>
2489                           <property name="padding">0</property>
2490                           <property name="expand">False</property>
2491                           <property name="fill">False</property>
2492                         </packing>
2493                       </child>
2494
2495                       <child>
2496                         <widget class="GtkLabel" id="label3">
2497                           <property name="visible">True</property>
2498                           <property name="label" translatable="yes">Try _Selected</property>
2499                           <property name="use_underline">True</property>
2500                           <property name="use_markup">False</property>
2501                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2502                           <property name="wrap">False</property>
2503                           <property name="selectable">False</property>
2504                           <property name="xalign">0.5</property>
2505                           <property name="yalign">0.5</property>
2506                           <property name="xpad">0</property>
2507                           <property name="ypad">0</property>
2508                         </widget>
2509                         <packing>
2510                           <property name="padding">0</property>
2511                           <property name="expand">False</property>
2512                           <property name="fill">False</property>
2513                         </packing>
2514                       </child>
2515                     </widget>
2516                   </child>
2517                 </widget>
2518               </child>
2519             </widget>
2520           </child>
2521
2522           <child>
2523             <widget class="GtkButton" id="UriChoiceConstantsButton">
2524               <property name="visible">True</property>
2525               <property name="sensitive">False</property>
2526               <property name="can_default">True</property>
2527               <property name="can_focus">True</property>
2528               <property name="label" translatable="yes">Try Constants</property>
2529               <property name="use_underline">True</property>
2530               <property name="relief">GTK_RELIEF_NORMAL</property>
2531               <property name="focus_on_click">True</property>
2532               <property name="response_id">0</property>
2533             </widget>
2534           </child>
2535
2536           <child>
2537             <widget class="GtkButton" id="copyButton">
2538               <property name="can_default">True</property>
2539               <property name="can_focus">True</property>
2540               <property name="label">gtk-copy</property>
2541               <property name="use_stock">True</property>
2542               <property name="relief">GTK_RELIEF_NORMAL</property>
2543               <property name="focus_on_click">True</property>
2544               <property name="response_id">0</property>
2545             </widget>
2546           </child>
2547
2548           <child>
2549             <widget class="GtkButton" id="uriChoiceAutoButton">
2550               <property name="visible">True</property>
2551               <property name="can_default">True</property>
2552               <property name="can_focus">True</property>
2553               <property name="relief">GTK_RELIEF_NORMAL</property>
2554               <property name="focus_on_click">True</property>
2555               <property name="response_id">0</property>
2556
2557               <child>
2558                 <widget class="GtkAlignment" id="alignment5">
2559                   <property name="visible">True</property>
2560                   <property name="xalign">0.5</property>
2561                   <property name="yalign">0.5</property>
2562                   <property name="xscale">0</property>
2563                   <property name="yscale">0</property>
2564                   <property name="top_padding">0</property>
2565                   <property name="bottom_padding">0</property>
2566                   <property name="left_padding">0</property>
2567                   <property name="right_padding">0</property>
2568
2569                   <child>
2570                     <widget class="GtkHBox" id="hbox16">
2571                       <property name="visible">True</property>
2572                       <property name="homogeneous">False</property>
2573                       <property name="spacing">2</property>
2574
2575                       <child>
2576                         <widget class="GtkImage" id="image302">
2577                           <property name="visible">True</property>
2578                           <property name="stock">gtk-ok</property>
2579                           <property name="icon_size">4</property>
2580                           <property name="xalign">0.5</property>
2581                           <property name="yalign">0.5</property>
2582                           <property name="xpad">0</property>
2583                           <property name="ypad">0</property>
2584                         </widget>
2585                         <packing>
2586                           <property name="padding">0</property>
2587                           <property name="expand">False</property>
2588                           <property name="fill">False</property>
2589                         </packing>
2590                       </child>
2591
2592                       <child>
2593                         <widget class="GtkLabel" id="okLabel">
2594                           <property name="visible">True</property>
2595                           <property name="label" translatable="yes">bla bla bla</property>
2596                           <property name="use_underline">True</property>
2597                           <property name="use_markup">False</property>
2598                           <property name="justify">GTK_JUSTIFY_LEFT</property>
2599                           <property name="wrap">False</property>
2600                           <property name="selectable">False</property>
2601                           <property name="xalign">0.5</property>
2602                           <property name="yalign">0.5</property>
2603                           <property name="xpad">0</property>
2604                           <property name="ypad">0</property>
2605                         </widget>
2606                         <packing>
2607                           <property name="padding">0</property>
2608                           <property name="expand">False</property>
2609                           <property name="fill">False</property>
2610                         </packing>
2611                       </child>
2612                     </widget>
2613                   </child>
2614                 </widget>
2615               </child>
2616             </widget>
2617           </child>
2618         </widget>
2619         <packing>
2620           <property name="padding">0</property>
2621           <property name="expand">False</property>
2622           <property name="fill">True</property>
2623           <property name="pack_type">GTK_PACK_END</property>
2624         </packing>
2625       </child>
2626
2627       <child>
2628         <widget class="GtkVBox" id="vbox2">
2629           <property name="visible">True</property>
2630           <property name="homogeneous">False</property>
2631           <property name="spacing">3</property>
2632
2633           <child>
2634             <widget class="GtkLabel" id="UriChoiceLabel">
2635               <property name="visible">True</property>
2636               <property name="label" translatable="yes">some informative message here ...</property>
2637               <property name="use_underline">False</property>
2638               <property name="use_markup">False</property>
2639               <property name="justify">GTK_JUSTIFY_LEFT</property>
2640               <property name="wrap">False</property>
2641               <property name="selectable">False</property>
2642               <property name="xalign">0.5</property>
2643               <property name="yalign">0.5</property>
2644               <property name="xpad">0</property>
2645               <property name="ypad">0</property>
2646             </widget>
2647             <packing>
2648               <property name="padding">0</property>
2649               <property name="expand">False</property>
2650               <property name="fill">False</property>
2651             </packing>
2652           </child>
2653
2654           <child>
2655             <widget class="GtkScrolledWindow" id="scrolledwindow1">
2656               <property name="width_request">400</property>
2657               <property name="visible">True</property>
2658               <property name="can_focus">True</property>
2659               <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2660               <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
2661               <property name="shadow_type">GTK_SHADOW_NONE</property>
2662               <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
2663
2664               <child>
2665                 <widget class="GtkTreeView" id="UriChoiceTreeView">
2666                   <property name="visible">True</property>
2667                   <property name="can_focus">True</property>
2668                   <property name="headers_visible">False</property>
2669                   <property name="rules_hint">False</property>
2670                   <property name="reorderable">False</property>
2671                   <property name="enable_search">True</property>
2672                 </widget>
2673               </child>
2674             </widget>
2675             <packing>
2676               <property name="padding">0</property>
2677               <property name="expand">True</property>
2678               <property name="fill">True</property>
2679             </packing>
2680           </child>
2681
2682           <child>
2683             <widget class="GtkHBox" id="uriEntryHBox">
2684               <property name="visible">True</property>
2685               <property name="homogeneous">False</property>
2686               <property name="spacing">0</property>
2687
2688               <child>
2689                 <widget class="GtkLabel" id="label2">
2690                   <property name="visible">True</property>
2691                   <property name="label" translatable="yes">URI: </property>
2692                   <property name="use_underline">False</property>
2693                   <property name="use_markup">False</property>
2694                   <property name="justify">GTK_JUSTIFY_LEFT</property>
2695                   <property name="wrap">False</property>
2696                   <property name="selectable">False</property>
2697                   <property name="xalign">0.5</property>
2698                   <property name="yalign">0.5</property>
2699                   <property name="xpad">0</property>
2700                   <property name="ypad">0</property>
2701                 </widget>
2702                 <packing>
2703                   <property name="padding">0</property>
2704                   <property name="expand">False</property>
2705                   <property name="fill">False</property>
2706                 </packing>
2707               </child>
2708
2709               <child>
2710                 <widget class="GtkEntry" id="entry1">
2711                   <property name="visible">True</property>
2712                   <property name="can_focus">True</property>
2713                   <property name="editable">True</property>
2714                   <property name="visibility">True</property>
2715                   <property name="max_length">0</property>
2716                   <property name="text" translatable="yes"></property>
2717                   <property name="has_frame">True</property>
2718                   <property name="invisible_char">*</property>
2719                   <property name="activates_default">False</property>
2720                 </widget>
2721                 <packing>
2722                   <property name="padding">0</property>
2723                   <property name="expand">True</property>
2724                   <property name="fill">True</property>
2725                 </packing>
2726               </child>
2727             </widget>
2728             <packing>
2729               <property name="padding">0</property>
2730               <property name="expand">False</property>
2731               <property name="fill">True</property>
2732             </packing>
2733           </child>
2734         </widget>
2735         <packing>
2736           <property name="padding">0</property>
2737           <property name="expand">True</property>
2738           <property name="fill">True</property>
2739         </packing>
2740       </child>
2741     </widget>
2742   </child>
2743 </widget>
2744
2745 </glade-interface>