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