* Hbugs interface clean-up.

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1c81ddbbfbc72f6882d67fa5f569c480a87eb9fd..9bd242eb8ad46ee3fa9e35934c28e089aaba663c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -574,7 +574,17 @@ let refresh_proof (output : TermViewer.proof_viewer) =
    match !ProofEngine.proof with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
-       !qed_set_sensitive (List.length metasenv = 0) ;
+       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, []))
@@ -647,7 +657,6 @@ let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
       raise (InvokeTactics.RefreshSequentException e)
 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
 
-let __notify_hbugs = ref None;;
 module InvokeTacticsCallbacks =
  struct
   let sequent_viewer () = (rendering_window ())#notebook#proofw
@@ -665,15 +674,11 @@ module InvokeTacticsCallbacks =
   let decompose_uris_choice_callback = decompose_uris_choice_callback
   let mk_fresh_name_callback = mk_fresh_name_callback
   let output_html msg = output_html (outputhtml ()) msg
-  let notify_hbugs () =
-    match !__notify_hbugs with
-    | Some f -> f ()
-    | None -> assert false
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-module Hbugs' = Hbugs.Make (InvokeTactics');;
-__notify_hbugs := Some Hbugs'.notify;;
+(* Just to initialize the Hbugs module *)
+module Ignore = Hbugs.Initialize (InvokeTactics');;
 
   (** load an unfinished proof from filesystem *)
 let load_unfinished_proof () =
@@ -707,7 +712,6 @@ let load_unfinished_proof () =
               ("<h1 color=\"Green\">Current proof body loaded from " ^
                 prooffile ^ "</h1>") ;
             !save_set_sensitive true;
-            Hbugs'.notify ()
          | _ -> assert false
   with
      InvokeTactics.RefreshSequentException e ->
@@ -1565,7 +1569,6 @@ let new_proof () =
      !save_set_sensitive true ;
      inputt#reset ;
      ProofEngine.intros ~mk_fresh_name_callback () ;
-     Hbugs'.notify ();
      refresh_goals notebook ;
      refresh_proof output
   with
@@ -2748,7 +2751,7 @@ class rendering_window output (notebook : notebook) =
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
  let toggle_hbugs_menu_item =
   factory6#add_check_item
-    ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled"
+    ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
@@ -2843,7 +2846,7 @@ let initialize_everything () =
      Gdome_xslt.setDebugCallback
       (Some (print_error_as_html "XSLT Debug Message: "));
      rendering_window'#show () ;
-(*      Hbugs'.toggle true; *)
+(*      Hbugs.toggle true; *)
      GtkThread.main ()
 ;;
 
@@ -2857,7 +2860,7 @@ let main () =
  initialize_everything () ;
  if !usedb then Mqint.close ();
  prerr_endline "FOO";
- Hbugs'.quit ()
+ Hbugs.quit ()
 ;;
 
 try