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