- added a destroy callback

- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index d9512d26cfcbf732dc7ec2ab194837fdf58d0a2a..4e009322c846b9e2f4423c79ca1a8eb6456943b7 100644 (file)
--- a/helm/hbugs/client/hbugs_client.ml
+++ b/helm/hbugs/client/hbugs_client.ml
@@ -34,6 +34,8 @@ exception Invalid_URL of string;;
 
 let global_debug = true;;
 
+let do_nothing _ = ();;
+
   (**
   @param on_use_hint function invoked when an hint is used, argumnet is the hint
   to use
@@ -41,7 +43,8 @@ let global_debug = true;;
   destroyed, if it's None "self#quit" is invoked
   *)
 class hbugsClient
-  ?(use_hint_callback: hint -> unit = (fun _ -> ()))
+  ?(use_hint_callback: hint -> unit = do_nothing)
+  ?(destroy_callback: unit -> unit = do_nothing)
   ()
   =
 
@@ -97,11 +100,14 @@ class hbugsClient
     method private initGui =
 
         (* GUI: main window *)
-      let on_exit = fun () -> self#quit (); false in
+
+          (* ignore delete events so that hbugs window is closable only using
+          menu; on destroy (e.g. while quitting gTopLevel) self#quit is invoked
+          *)
+
+      ignore (mainWindow#hbugsMainWindow#event#connect#delete (fun _ -> true));
       ignore (mainWindow#hbugsMainWindow#event#connect#destroy
-        (fun _ -> on_exit ()));
-      ignore (mainWindow#hbugsMainWindow#event#connect#delete
-        (fun _ -> on_exit ()));
+        (fun _ -> self#quit (); false));
 
         (* GUI main window's menu *)
       mainWindow#toggleDebuggingMenuItem#set_active debug;
@@ -395,7 +401,7 @@ Error: %s"
 
     method private quit () =
       self#unregisterFromBroker ();
-      GMain.Main.quit ()
+      destroy_callback ()
 
       (** enable/disable debugging *)
     method private setDebug value = debug <- value

diff --git a/helm/hbugs/client/hbugs_client.mli b/helm/hbugs/client/hbugs_client.mli
index cf7ebc2a991a0aaf112f7e6e668cc2922d07832a..87e11e968501ca75183785b5d04f69a7328cf575 100644 (file)
--- a/helm/hbugs/client/hbugs_client.mli
+++ b/helm/hbugs/client/hbugs_client.mli
@@ -4,7 +4,8 @@ open Hbugs_types
 exception Invalid_URL of string
 
 class hbugsClient :
-  ?use_hint_callback: (hint -> unit) ->
+  ?use_hint_callback: (hint -> unit) -> (* default = do nothing *)
+  ?destroy_callback: (unit -> unit) ->  (* default = do nothing *)
   unit ->
     object