X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fclient%2Fhbugs_client.ml;h=4e009322c846b9e2f4423c79ca1a8eb6456943b7;hb=22bb9330d93cdf89baa5df76df6db72709a4d6fb;hp=d9512d26cfcbf732dc7ec2ab194837fdf58d0a2a;hpb=641aec825f4cf10d5075da92681575acdfeeb2ae;p=helm.git

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