From f80986dd44466287251d58367b021870de22ba7b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 4 Sep 2003 16:43:25 +0000 Subject: [PATCH] - 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 --- helm/gTopLevel/gTopLevel.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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 -- 2.39.2