From 22bb9330d93cdf89baa5df76df6db72709a4d6fb Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 4 Sep 2003 16:46:46 +0000
Subject: [PATCH] - added a destroy callback - ignore delete events on hbugs
 window - unsubscribe only when hbugs window gets _destroyed_

---
 helm/hbugs/client/hbugs_client.ml  | 18 ++++++++++++------
 helm/hbugs/client/hbugs_client.mli |  3 ++-
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index d9512d26c..4e009322c 100644
--- 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 cf7ebc2a9..87e11e968 100644
--- 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
 
-- 
2.39.2