From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 4 Sep 2003 16:43:25 +0000 (+0000)
Subject: - added default URI for new theorems
X-Git-Tag: v0_0_1~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f80986dd44466287251d58367b021870de22ba7b;p=helm.git

- added default URI for new theorems
- added menu items to the hbugs menu for:
  * start and stop hbugs web services
  * force submission of current status
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 65f381859..a7ec39e09 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1482,6 +1482,9 @@ let new_proof () =
  let uri_entry =
   GEdit.entry ~editable:true
    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let hint_uri = "/foo.con" in
+ uri_entry#set_text hint_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length hint_uri);
  let hbox1 =
   GPack.hbox ~border_width:0
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2742,10 +2745,18 @@ class rendering_window output (notebook : notebook) =
  (* hbugs menu *)
  let hbugs_menu = factory0#add_submenu "HBugs" in
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ let _ =
   factory6#add_check_item
     ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
+ let _ = factory6#add_item ~callback:Hbugs.notify "(Re)Submit status!" in
+ let _ = factory6#add_separator () in
+ let _ =
+  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+ in
+ let _ =
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in