X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=a7ec39e09e98768f531bc05757b953ba8d6877f0;hb=9ca6b45a45f1cc4cb30a4f36f9939dbedf657e6e;hp=f1710cfce134d60e09f8cdaa3f7d79492402b61e;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f1710cfce..a7ec39e09 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -561,6 +561,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
    match !ProofEngine.proof with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
+       ProofEngine.proof := Some(uri,metasenv,bo,ty);
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
@@ -1481,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
@@ -1912,10 +1916,10 @@ let completeSearchPattern () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
-   let must = MQueryLevels2.get_constraints expr in
+   let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
-    MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
@@ -2039,10 +2043,10 @@ let choose_must list_of_must only =
      in
       ignore
        (List.map
-         (function (uri,position) ->
+         (function (position, uri) ->
            let n =
             clist#append 
-             [uri; if position then "MainConclusion" else "Conclusion"]
+             [uri; MQGUtil.text_of_position position]
            in
             clist#set_row ~selectable:false n
          ) must
@@ -2071,10 +2075,10 @@ let choose_must list_of_must only =
   in
    ignore
     (List.map
-      (function (uri,position) ->
+      (function (position, uri) ->
         let n =
          clist#append 
-          [uri; if position then "MainConclusion" else "Conclusion"]
+          [uri; MQGUtil.text_of_position position]
         in
          clist#set_row ~selectable:true n
       ) only
@@ -2741,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