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