HBugs compile again (but it does not do anything right now: still to be

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 6aaec3aeda401c9e0f3f0472ebf4e2a3330cc5de..88d819fded0abd67afdc1a8f4a8dce14af9f1835 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -572,10 +572,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
-         (*Hbugs.clear*) ()
+         Hbugs.clear ()
         end
        else
-        (*Hbugs.notify*) () ;
+        Hbugs.notify () ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
@@ -674,7 +674,6 @@ module InvokeTacticsCallbacks =
 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
@@ -683,7 +682,6 @@ Hbugs.set_describe_hint_callback (fun hint ->
       check_window outputhtml [term]
   | _ -> ())
 ;;
-*)
 
 let dummy_uri = "/dummy.con"
 
@@ -2666,7 +2664,7 @@ object(self)
           Lazy.force (page#compute) ;
           Lazy.force setgoal;
           if notify_hbugs_on_goal_change then
-            (*Hbugs.notify *) ()
+            Hbugs.notify ()
         with _ -> ()
     ))
 end
@@ -2860,18 +2858,18 @@ class rendering_window output (notebook : notebook) =
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
  let _ =
   factory6#add_check_item
-    ~active:false ~key:GdkKeysyms._F5 ~callback:(*Hbugs.toggle*)(fun _ -> ()) "HBugs enabled"
+    ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
  let _ =
-  factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ())
+  factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
    "(Re)Submit status!"
  in
  let _ = factory6#add_separator () in
  let _ =
-  factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services"
+  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
  in
  let _ =
-  factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services"
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
  in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
@@ -2995,8 +2993,8 @@ let initialize_everything () =
 let main () =
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- MQIC.close mqi_handle(*;
- Hbugs.quit ()*)
+ MQIC.close mqi_handle;
+ Hbugs.quit ()
 ;;
 
 try