From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Apr 2003 14:14:45 +0000 (+0000)
Subject: - removed unclear parameter on_exit
X-Git-Tag: before_refactoring~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39559db1a359271e8794fe8e08c21afe73a581d9;p=helm.git

- removed unclear parameter on_exit
- renamed on_use_hint to use_hint_callback
- added method setUseHintCallback
---

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index 4a31f9a13..d9512d26c 100644
--- 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 *)
diff --git a/helm/hbugs/client/hbugs_client.mli b/helm/hbugs/client/hbugs_client.mli
index 3bc34a8e2..cf7ebc2a9 100644
--- a/helm/hbugs/client/hbugs_client.mli
+++ b/helm/hbugs/client/hbugs_client.mli
@@ -4,19 +4,19 @@ open Hbugs_types
 exception Invalid_URL of string
 
 class hbugsClient :
-  on_use_hint: (hint -> unit) ->
-  ?on_exit: (unit -> unit) ->
+  ?use_hint_callback: (hint -> unit) ->
   unit ->
     object
 
       method show : unit -> unit
       method hide : unit -> unit
 
+      method setUseHintCallback : (hint -> unit) -> unit
       method registerToBroker : unit -> unit
       method unregisterFromBroker : unit -> unit
       method subscribeAll : unit -> unit
 
-      method stateChange : state -> unit
+      method stateChange : state option -> unit
 
         (** @return an hint by index *)
       method hint : int -> hint
diff --git a/helm/hbugs/client/main.ml b/helm/hbugs/client/main.ml
index cfb4f8ba1..e694613c5 100644
--- a/helm/hbugs/client/main.ml
+++ b/helm/hbugs/client/main.ml
@@ -31,7 +31,7 @@ open Printf;;
 
 let client =
   new Hbugs_client.hbugsClient
-    ~on_use_hint:
+    ~use_hint_callback:
       (fun hint ->
         prerr_endline (sprintf "Using hint: %s" (string_of_hint hint)))
     ()