]> matita.cs.unibo.it Git - helm.git/blob - components/hbugs/hbugs_client_gui.glade
Added a new command "index" for the indexing terms in the "universe".
[helm.git] / components / hbugs / hbugs_client_gui.glade
1 <?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
2 <!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
3
4 <glade-interface>
5 <requires lib="gnome"/>
6
7 <widget class="GtkWindow" id="hbugsMainWindow">
8   <property name="title" translatable="yes">Hbugs: your personal proof trainer!</property>
9   <property name="type">GTK_WINDOW_TOPLEVEL</property>
10   <property name="window_position">GTK_WIN_POS_NONE</property>
11   <property name="modal">False</property>
12   <property name="resizable">True</property>
13   <property name="destroy_with_parent">False</property>
14
15   <child>
16     <widget class="GtkVBox" id="vbox1">
17       <property name="visible">True</property>
18       <property name="homogeneous">False</property>
19       <property name="spacing">0</property>
20
21       <child>
22         <widget class="GtkMenuBar" id="menubar">
23
24           <child>
25             <widget class="GtkMenuItem" id="toolsMenu">
26               <property name="visible">True</property>
27               <property name="label" translatable="yes">Tools</property>
28               <property name="use_underline">True</property>
29
30               <child>
31                 <widget class="GtkMenu" id="toolsMenu_menu">
32                   <property name="visible">True</property>
33
34                   <child>
35                     <widget class="GtkCheckMenuItem" id="toggleDebuggingMenuItem">
36                       <property name="visible">True</property>
37                       <property name="label" translatable="yes">Debugging</property>
38                       <property name="use_underline">True</property>
39                       <property name="active">False</property>
40                     </widget>
41                   </child>
42                 </widget>
43               </child>
44             </widget>
45           </child>
46         </widget>
47         <packing>
48           <property name="padding">0</property>
49           <property name="expand">False</property>
50           <property name="fill">False</property>
51         </packing>
52       </child>
53
54       <child>
55         <widget class="GtkHBox" id="hbox4">
56           <property name="visible">True</property>
57           <property name="homogeneous">False</property>
58           <property name="spacing">2</property>
59
60           <child>
61             <widget class="GtkLabel" id="label11">
62               <property name="visible">True</property>
63               <property name="label" translatable="yes">My URL:</property>
64               <property name="use_underline">False</property>
65               <property name="use_markup">False</property>
66               <property name="justify">GTK_JUSTIFY_CENTER</property>
67               <property name="wrap">False</property>
68               <property name="selectable">False</property>
69               <property name="xalign">0.5</property>
70               <property name="yalign">0.5</property>
71               <property name="xpad">0</property>
72               <property name="ypad">0</property>
73             </widget>
74             <packing>
75               <property name="padding">0</property>
76               <property name="expand">False</property>
77               <property name="fill">False</property>
78             </packing>
79           </child>
80
81           <child>
82             <widget class="GtkEntry" id="clientUrlEntry">
83               <property name="visible">True</property>
84               <property name="tooltip" translatable="yes">Local HTTP daemon URL</property>
85               <property name="can_focus">True</property>
86               <property name="editable">False</property>
87               <property name="visibility">True</property>
88               <property name="max_length">0</property>
89               <property name="text" translatable="yes"></property>
90               <property name="has_frame">True</property>
91               <property name="invisible_char" translatable="yes">*</property>
92               <property name="activates_default">False</property>
93             </widget>
94             <packing>
95               <property name="padding">0</property>
96               <property name="expand">True</property>
97               <property name="fill">True</property>
98             </packing>
99           </child>
100
101           <child>
102             <widget class="GtkButton" id="startLocalHttpDaemonButton">
103               <property name="visible">True</property>
104               <property name="tooltip" translatable="yes">Start the local HTTP daemon listening on the specified URL</property>
105               <property name="can_focus">True</property>
106               <property name="label" translatable="yes">Start!</property>
107               <property name="use_underline">True</property>
108               <property name="relief">GTK_RELIEF_NORMAL</property>
109             </widget>
110             <packing>
111               <property name="padding">0</property>
112               <property name="expand">False</property>
113               <property name="fill">False</property>
114             </packing>
115           </child>
116
117           <child>
118             <widget class="GtkButton" id="testLocalHttpDaemonButton">
119               <property name="visible">True</property>
120               <property name="can_focus">True</property>
121               <property name="label" translatable="yes">Test!</property>
122               <property name="use_underline">True</property>
123               <property name="relief">GTK_RELIEF_NORMAL</property>
124             </widget>
125             <packing>
126               <property name="padding">0</property>
127               <property name="expand">False</property>
128               <property name="fill">False</property>
129             </packing>
130           </child>
131         </widget>
132         <packing>
133           <property name="padding">0</property>
134           <property name="expand">False</property>
135           <property name="fill">False</property>
136         </packing>
137       </child>
138
139       <child>
140         <widget class="GtkVBox" id="vbox4">
141           <property name="visible">True</property>
142           <property name="homogeneous">False</property>
143           <property name="spacing">0</property>
144
145           <child>
146             <widget class="GtkHBox" id="hbox1">
147               <property name="visible">True</property>
148               <property name="homogeneous">False</property>
149               <property name="spacing">2</property>
150
151               <child>
152                 <widget class="GtkLabel" id="label1">
153                   <property name="visible">True</property>
154                   <property name="label" translatable="yes">Broker:</property>
155                   <property name="use_underline">False</property>
156                   <property name="use_markup">False</property>
157                   <property name="justify">GTK_JUSTIFY_CENTER</property>
158                   <property name="wrap">False</property>
159                   <property name="selectable">False</property>
160                   <property name="xalign">0.5</property>
161                   <property name="yalign">0.5</property>
162                   <property name="xpad">0</property>
163                   <property name="ypad">0</property>
164                 </widget>
165                 <packing>
166                   <property name="padding">0</property>
167                   <property name="expand">False</property>
168                   <property name="fill">False</property>
169                 </packing>
170               </child>
171
172               <child>
173                 <widget class="GtkEntry" id="brokerUrlEntry">
174                   <property name="visible">True</property>
175                   <property name="tooltip" translatable="yes">HBugs broker URL</property>
176                   <property name="can_focus">True</property>
177                   <property name="editable">False</property>
178                   <property name="visibility">True</property>
179                   <property name="max_length">0</property>
180                   <property name="text" translatable="yes"></property>
181                   <property name="has_frame">True</property>
182                   <property name="invisible_char" translatable="yes">*</property>
183                   <property name="activates_default">False</property>
184                 </widget>
185                 <packing>
186                   <property name="padding">0</property>
187                   <property name="expand">True</property>
188                   <property name="fill">True</property>
189                 </packing>
190               </child>
191
192               <child>
193                 <widget class="GtkButton" id="testBrokerButton">
194                   <property name="visible">True</property>
195                   <property name="can_focus">True</property>
196                   <property name="label" translatable="yes">Test!</property>
197                   <property name="use_underline">True</property>
198                   <property name="relief">GTK_RELIEF_NORMAL</property>
199                 </widget>
200                 <packing>
201                   <property name="padding">0</property>
202                   <property name="expand">False</property>
203                   <property name="fill">False</property>
204                 </packing>
205               </child>
206             </widget>
207             <packing>
208               <property name="padding">0</property>
209               <property name="expand">False</property>
210               <property name="fill">False</property>
211             </packing>
212           </child>
213
214           <child>
215             <widget class="GtkHBox" id="hbox2">
216               <property name="visible">True</property>
217               <property name="homogeneous">False</property>
218               <property name="spacing">2</property>
219
220               <child>
221                 <widget class="GtkLabel" id="label2">
222                   <property name="label" translatable="yes">Client ID:</property>
223                   <property name="use_underline">False</property>
224                   <property name="use_markup">False</property>
225                   <property name="justify">GTK_JUSTIFY_CENTER</property>
226                   <property name="wrap">False</property>
227                   <property name="selectable">False</property>
228                   <property name="xalign">0.5</property>
229                   <property name="yalign">0.5</property>
230                   <property name="xpad">0</property>
231                   <property name="ypad">0</property>
232                 </widget>
233                 <packing>
234                   <property name="padding">0</property>
235                   <property name="expand">False</property>
236                   <property name="fill">False</property>
237                 </packing>
238               </child>
239
240               <child>
241                 <widget class="GtkLabel" id="clientIdLabel">
242                   <property name="label" translatable="yes"></property>
243                   <property name="use_underline">False</property>
244                   <property name="use_markup">False</property>
245                   <property name="justify">GTK_JUSTIFY_LEFT</property>
246                   <property name="wrap">False</property>
247                   <property name="selectable">False</property>
248                   <property name="xalign">0.5</property>
249                   <property name="yalign">0.5</property>
250                   <property name="xpad">0</property>
251                   <property name="ypad">0</property>
252                 </widget>
253                 <packing>
254                   <property name="padding">0</property>
255                   <property name="expand">True</property>
256                   <property name="fill">True</property>
257                 </packing>
258               </child>
259
260               <child>
261                 <widget class="GtkButton" id="registerClientButton">
262                   <property name="visible">True</property>
263                   <property name="can_focus">True</property>
264                   <property name="label" translatable="yes">(Re)Register</property>
265                   <property name="use_underline">True</property>
266                   <property name="relief">GTK_RELIEF_NORMAL</property>
267                 </widget>
268                 <packing>
269                   <property name="padding">0</property>
270                   <property name="expand">False</property>
271                   <property name="fill">False</property>
272                 </packing>
273               </child>
274             </widget>
275             <packing>
276               <property name="padding">0</property>
277               <property name="expand">False</property>
278               <property name="fill">False</property>
279             </packing>
280           </child>
281         </widget>
282         <packing>
283           <property name="padding">0</property>
284           <property name="expand">False</property>
285           <property name="fill">True</property>
286         </packing>
287       </child>
288
289       <child>
290         <widget class="GtkVPaned" id="vpaned1">
291           <property name="visible">True</property>
292           <property name="position">0</property>
293
294           <child>
295             <widget class="GtkFrame" id="frame3">
296               <property name="border_width">4</property>
297               <property name="visible">True</property>
298               <property name="label_xalign">0</property>
299               <property name="label_yalign">0.5</property>
300               <property name="shadow_type">GTK_SHADOW_ETCHED_IN</property>
301
302               <child>
303                 <widget class="GtkHBox" id="hbox6">
304                   <property name="visible">True</property>
305                   <property name="homogeneous">False</property>
306                   <property name="spacing">2</property>
307
308                   <child>
309                     <widget class="GtkScrolledWindow" id="scrolledwindow3">
310                       <property name="visible">True</property>
311                       <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
312                       <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
313                       <property name="shadow_type">GTK_SHADOW_IN</property>
314                       <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
315
316                       <child>
317                         <widget class="GtkTreeView" id="subscriptionCList">
318                           <property name="visible">True</property>
319                           <property name="can_focus">True</property>
320                           <property name="headers_visible">True</property>
321                           <property name="rules_hint">False</property>
322                           <property name="reorderable">False</property>
323                           <property name="enable_search">True</property>
324                         </widget>
325                       </child>
326                     </widget>
327                     <packing>
328                       <property name="padding">0</property>
329                       <property name="expand">True</property>
330                       <property name="fill">True</property>
331                     </packing>
332                   </child>
333
334                   <child>
335                     <widget class="GtkFixed" id="fixed1">
336                       <property name="visible">True</property>
337
338                       <child>
339                         <widget class="GtkButton" id="showSubscriptionWindowButton">
340                           <property name="width_request">0</property>
341                           <property name="height_request">0</property>
342                           <property name="visible">True</property>
343                           <property name="can_focus">True</property>
344                           <property name="label" translatable="yes">Subscribe ...</property>
345                           <property name="use_underline">True</property>
346                           <property name="relief">GTK_RELIEF_NORMAL</property>
347                         </widget>
348                         <packing>
349                           <property name="x">0</property>
350                           <property name="y">0</property>
351                         </packing>
352                       </child>
353                     </widget>
354                     <packing>
355                       <property name="padding">0</property>
356                       <property name="expand">False</property>
357                       <property name="fill">False</property>
358                     </packing>
359                   </child>
360                 </widget>
361               </child>
362
363               <child>
364                 <widget class="GtkLabel" id="label12">
365                   <property name="visible">True</property>
366                   <property name="label" translatable="yes">Subscriptions</property>
367                   <property name="use_underline">False</property>
368                   <property name="use_markup">False</property>
369                   <property name="justify">GTK_JUSTIFY_LEFT</property>
370                   <property name="wrap">False</property>
371                   <property name="selectable">False</property>
372                   <property name="xalign">0.5</property>
373                   <property name="yalign">0.5</property>
374                   <property name="xpad">0</property>
375                   <property name="ypad">0</property>
376                 </widget>
377                 <packing>
378                   <property name="type">label_item</property>
379                 </packing>
380               </child>
381             </widget>
382             <packing>
383               <property name="shrink">False</property>
384               <property name="resize">False</property>
385             </packing>
386           </child>
387
388           <child>
389             <widget class="GtkFrame" id="frame2">
390               <property name="border_width">4</property>
391               <property name="visible">True</property>
392               <property name="label_xalign">0</property>
393               <property name="label_yalign">0.5</property>
394               <property name="shadow_type">GTK_SHADOW_ETCHED_IN</property>
395
396               <child>
397                 <widget class="GtkVBox" id="vbox6">
398                   <property name="visible">True</property>
399                   <property name="homogeneous">False</property>
400                   <property name="spacing">0</property>
401
402                   <child>
403                     <widget class="GtkScrolledWindow" id="scrolledwindow2">
404                       <property name="visible">True</property>
405                       <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
406                       <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
407                       <property name="shadow_type">GTK_SHADOW_IN</property>
408                       <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
409
410                       <child>
411                         <widget class="GtkTreeView" id="hintsCList">
412                           <property name="visible">True</property>
413                           <property name="can_focus">True</property>
414                           <property name="headers_visible">True</property>
415                           <property name="rules_hint">False</property>
416                           <property name="reorderable">False</property>
417                           <property name="enable_search">True</property>
418                         </widget>
419                       </child>
420                     </widget>
421                     <packing>
422                       <property name="padding">0</property>
423                       <property name="expand">True</property>
424                       <property name="fill">True</property>
425                     </packing>
426                   </child>
427                 </widget>
428               </child>
429
430               <child>
431                 <widget class="GtkLabel" id="label13">
432                   <property name="visible">True</property>
433                   <property name="label" translatable="yes">Hints</property>
434                   <property name="use_underline">False</property>
435                   <property name="use_markup">False</property>
436                   <property name="justify">GTK_JUSTIFY_LEFT</property>
437                   <property name="wrap">False</property>
438                   <property name="selectable">False</property>
439                   <property name="xalign">0.5</property>
440                   <property name="yalign">0.5</property>
441                   <property name="xpad">0</property>
442                   <property name="ypad">0</property>
443                 </widget>
444                 <packing>
445                   <property name="type">label_item</property>
446                 </packing>
447               </child>
448             </widget>
449             <packing>
450               <property name="shrink">True</property>
451               <property name="resize">True</property>
452             </packing>
453           </child>
454         </widget>
455         <packing>
456           <property name="padding">0</property>
457           <property name="expand">True</property>
458           <property name="fill">True</property>
459         </packing>
460       </child>
461
462       <child>
463         <widget class="GtkStatusbar" id="mainWindowStatusBar">
464           <property name="has_resize_grip">True</property>
465         </widget>
466         <packing>
467           <property name="padding">0</property>
468           <property name="expand">False</property>
469           <property name="fill">False</property>
470         </packing>
471       </child>
472     </widget>
473   </child>
474 </widget>
475
476 <widget class="GtkWindow" id="subscribeWindow">
477   <property name="title" translatable="yes">Hbugs: subscribe ...</property>
478   <property name="type">GTK_WINDOW_TOPLEVEL</property>
479   <property name="window_position">GTK_WIN_POS_NONE</property>
480   <property name="modal">False</property>
481   <property name="resizable">True</property>
482   <property name="destroy_with_parent">False</property>
483
484   <child>
485     <widget class="GtkVBox" id="vbox8">
486       <property name="visible">True</property>
487       <property name="homogeneous">False</property>
488       <property name="spacing">0</property>
489
490       <child>
491         <widget class="GtkButton" id="listTutorsButton">
492           <property name="visible">True</property>
493           <property name="can_focus">True</property>
494           <property name="label" translatable="yes">Refresh</property>
495           <property name="use_underline">True</property>
496           <property name="relief">GTK_RELIEF_NORMAL</property>
497         </widget>
498         <packing>
499           <property name="padding">0</property>
500           <property name="expand">False</property>
501           <property name="fill">False</property>
502         </packing>
503       </child>
504
505       <child>
506         <widget class="GtkScrolledWindow" id="scrolledwindow4">
507           <property name="visible">True</property>
508           <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
509           <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
510           <property name="shadow_type">GTK_SHADOW_IN</property>
511           <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
512
513           <child>
514             <widget class="GtkTreeView" id="tutorsCList">
515               <property name="visible">True</property>
516               <property name="can_focus">True</property>
517               <property name="headers_visible">True</property>
518               <property name="rules_hint">False</property>
519               <property name="reorderable">False</property>
520               <property name="enable_search">True</property>
521             </widget>
522           </child>
523         </widget>
524         <packing>
525           <property name="padding">0</property>
526           <property name="expand">True</property>
527           <property name="fill">True</property>
528         </packing>
529       </child>
530
531       <child>
532         <widget class="GtkHBox" id="hbox5">
533           <property name="visible">True</property>
534           <property name="homogeneous">False</property>
535           <property name="spacing">0</property>
536
537           <child>
538             <widget class="GtkButton" id="subscribeButton">
539               <property name="visible">True</property>
540               <property name="can_focus">True</property>
541               <property name="label" translatable="yes">Subscribe to Selected</property>
542               <property name="use_underline">True</property>
543               <property name="relief">GTK_RELIEF_NORMAL</property>
544             </widget>
545             <packing>
546               <property name="padding">0</property>
547               <property name="expand">True</property>
548               <property name="fill">True</property>
549             </packing>
550           </child>
551
552           <child>
553             <widget class="GtkButton" id="subscribeAllButton">
554               <property name="visible">True</property>
555               <property name="can_focus">True</property>
556               <property name="label" translatable="yes">Subscribe to All</property>
557               <property name="use_underline">True</property>
558               <property name="relief">GTK_RELIEF_NORMAL</property>
559             </widget>
560             <packing>
561               <property name="padding">0</property>
562               <property name="expand">True</property>
563               <property name="fill">True</property>
564             </packing>
565           </child>
566         </widget>
567         <packing>
568           <property name="padding">0</property>
569           <property name="expand">False</property>
570           <property name="fill">False</property>
571         </packing>
572       </child>
573
574       <child>
575         <widget class="GtkStatusbar" id="subscribeWindowStatusBar">
576           <property name="visible">True</property>
577           <property name="has_resize_grip">True</property>
578         </widget>
579         <packing>
580           <property name="padding">0</property>
581           <property name="expand">False</property>
582           <property name="fill">False</property>
583         </packing>
584       </child>
585     </widget>
586   </child>
587 </widget>
588
589 <widget class="GtkDialog" id="messageDialog">
590   <property name="title" translatable="yes">Message</property>
591   <property name="type">GTK_WINDOW_TOPLEVEL</property>
592   <property name="window_position">GTK_WIN_POS_NONE</property>
593   <property name="modal">True</property>
594   <property name="default_width">220</property>
595   <property name="default_height">150</property>
596   <property name="resizable">True</property>
597   <property name="destroy_with_parent">False</property>
598   <property name="has_separator">True</property>
599
600   <child internal-child="vbox">
601     <widget class="GtkVBox" id="dialogVbox1">
602       <property name="visible">True</property>
603       <property name="homogeneous">False</property>
604       <property name="spacing">0</property>
605
606       <child internal-child="action_area">
607         <widget class="GtkHButtonBox" id="dialogAction_area1">
608           <property name="visible">True</property>
609           <property name="layout_style">GTK_BUTTONBOX_END</property>
610
611           <child>
612             <widget class="GtkButton" id="okDialogButton">
613               <property name="visible">True</property>
614               <property name="can_focus">True</property>
615               <property name="label" translatable="yes">OK</property>
616               <property name="use_underline">True</property>
617               <property name="relief">GTK_RELIEF_NORMAL</property>
618               <property name="response_id">0</property>
619             </widget>
620           </child>
621         </widget>
622         <packing>
623           <property name="padding">0</property>
624           <property name="expand">False</property>
625           <property name="fill">True</property>
626           <property name="pack_type">GTK_PACK_END</property>
627         </packing>
628       </child>
629
630       <child>
631         <widget class="GtkTable" id="table1">
632           <property name="border_width">5</property>
633           <property name="visible">True</property>
634           <property name="n_rows">1</property>
635           <property name="n_columns">1</property>
636           <property name="homogeneous">False</property>
637           <property name="row_spacing">0</property>
638           <property name="column_spacing">0</property>
639
640           <child>
641             <widget class="GtkLabel" id="dialogLabel">
642               <property name="visible">True</property>
643               <property name="label" translatable="yes"></property>
644               <property name="use_underline">False</property>
645               <property name="use_markup">False</property>
646               <property name="justify">GTK_JUSTIFY_CENTER</property>
647               <property name="wrap">True</property>
648               <property name="selectable">False</property>
649               <property name="xalign">0.5</property>
650               <property name="yalign">0.5</property>
651               <property name="xpad">0</property>
652               <property name="ypad">0</property>
653             </widget>
654             <packing>
655               <property name="left_attach">0</property>
656               <property name="right_attach">1</property>
657               <property name="top_attach">0</property>
658               <property name="bottom_attach">1</property>
659             </packing>
660           </child>
661         </widget>
662         <packing>
663           <property name="padding">0</property>
664           <property name="expand">True</property>
665           <property name="fill">True</property>
666         </packing>
667       </child>
668     </widget>
669   </child>
670 </widget>
671
672 </glade-interface>