- the mathql interpreter is not helm-dependent any more

[helm.git] / helm / hbugs / client / hbugs_client.ml

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index 4a31f9a13a2a05e23f8bc61ef5d4e7c0d4e0f7ce..d9512d26cfcbf732dc7ec2ab194837fdf58d0a2a 100644 (file)
--- a/helm/hbugs/client/hbugs_client.ml
+++ b/helm/hbugs/client/hbugs_client.ml
@@ -41,8 +41,7 @@ let global_debug = true;;
   destroyed, if it's None "self#quit" is invoked
   *)
 class hbugsClient
-  ~(on_use_hint: hint -> unit)
-  ?(on_exit: (unit -> unit) option)
+  ?(use_hint_callback: hint -> unit = (fun _ -> ()))
   ()
   =
 
@@ -60,6 +59,7 @@ class hbugsClient
     val subscribeWindow = new Hbugs_client_gui.subscribeWindow ()
     val messageDialog = new Hbugs_client_gui.messageDialog ()
     val myOwnId = Hbugs_id_generator.new_client_id ()
+    val mutable use_hint_callback = use_hint_callback
     val mutable myOwnUrl = "localhost:49082"
     val mutable brokerUrl = "localhost:49081"
     val mutable brokerId: broker_id option = None
@@ -84,6 +84,9 @@ class hbugsClient
     method show = mainWindow#hbugsMainWindow#show
     method hide = mainWindow#hbugsMainWindow#misc#hide
 
+    method setUseHintCallback callback =
+     use_hint_callback <- callback
+
     method private debugButtons =
       List.map
         (fun (b: GButton.button) -> new GObj.misc_ops b#as_widget)
@@ -94,11 +97,7 @@ class hbugsClient
     method private initGui =
 
         (* GUI: main window *)
-      let on_exit =
-        match on_exit with
-        | None -> (fun () -> self#quit (); false)
-        | Some f -> (fun () -> f (); true)
-      in
+      let on_exit = fun () -> self#quit (); false in
       ignore (mainWindow#hbugsMainWindow#event#connect#destroy
         (fun _ -> on_exit ()));
       ignore (mainWindow#hbugsMainWindow#event#connect#delete
@@ -142,7 +141,7 @@ class hbugsClient
         (fun ~row ~column ~event ->
           match event with
           | Some event when GdkEvent.get_type event = `TWO_BUTTON_PRESS ->
-              on_use_hint (self#hint row)
+              use_hint_callback (self#hint row)
           | _ -> ()));
 
         (* GUI: main status bar *)