- use hbugs' describe_callback to render apply-hints on selection

- sync default uri proposed while loading a new proof and loading one
- resend status to hbugs on tab change

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index a7ec39e09e98768f531bc05757b953ba8d6877f0..9df5f8f75439f8966374aecf0260362c7c3a40fb 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -217,7 +217,8 @@ let check_window outputhtml uris =
  in
   ignore
    (notebook#connect#switch_page
-     (function i -> Lazy.force (List.nth render_terms i)))
+     (function i ->
+       Lazy.force (List.nth render_terms i)))
 ;;
 
 exception NoChoice;;
@@ -565,14 +566,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
          Hbugs.clear ()
         end
        else
-begin
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
         Hbugs.notify () ;
-end ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
@@ -665,8 +662,18 @@ module InvokeTacticsCallbacks =
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
+
 (* Just to initialize the Hbugs module *)
 module Ignore = Hbugs.Initialize (InvokeTactics');;
+Hbugs.set_describe_hint_callback (fun hint ->
+  match hint with
+  | Hbugs_types.Use_apply_Luke term ->
+      let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+      check_window outputhtml [term]
+  | _ -> ())
+;;
+
+let dummy_uri = "/dummy.con"
 
   (** load an unfinished proof from filesystem *)
 let load_unfinished_proof () =
@@ -675,7 +682,7 @@ let load_unfinished_proof () =
  let notebook = (rendering_window ())#notebook in
   try
    match 
-    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri
      "Choose an URI:"
    with
       None -> raise NoChoice
@@ -1482,9 +1489,8 @@ 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);
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
  let hbox1 =
   GPack.hbox ~border_width:0
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2638,7 +2644,8 @@ object(self)
          let (metano,setgoal,page) = List.nth !pages i in
           ProofEngine.goal := Some metano ;
           Lazy.force (page#compute) ;
-          Lazy.force setgoal
+          Lazy.force setgoal;
+          Hbugs.notify ()
         with _ -> ()
     ))
 end