helm/ocaml/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>