X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fclient%2Fhbugs_client.ml;h=1cab49c7609e361e7de3c52c9e498d941eafc443;hb=03d1ddf4a7fdf03fd497babd84d1963048253f0d;hp=4a31f9a13a2a05e23f8bc61ef5d4e7c0d4e0f7ce;hpb=594ea125d8bdd2c0a210e4b2170b0c725075d597;p=helm.git

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index 4a31f9a13..1cab49c76 100644
--- a/helm/hbugs/client/hbugs_client.ml
+++ b/helm/hbugs/client/hbugs_client.ml
@@ -32,17 +32,12 @@ open Printf;;
 
 exception Invalid_URL of string;;
 
-let global_debug = true;;
-
-  (**
-  @param on_use_hint function invoked when an hint is used, argumnet is the hint
-  to use
-  @param on_exit function invoked when client is exiting (e.g. window is
-  destroyed, if it's None "self#quit" is invoked
-  *)
+let do_nothing _ = ();;
+
 class hbugsClient
-  ~(on_use_hint: hint -> unit)
-  ?(on_exit: (unit -> unit) option)
+  ?(use_hint_callback: hint -> unit = do_nothing)
+  ?(describe_hint_callback: hint -> unit = do_nothing)
+  ?(destroy_callback: unit -> unit = do_nothing)
   ()
   =
 
@@ -60,6 +55,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,25 +80,26 @@ 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)
         [ mainWindow#startLocalHttpDaemonButton;
-        mainWindow#testLocalHttpDaemonButton; mainWindow#testBrokerButton;
-        mainWindow#registerClientButton; mainWindow#unregisterClientButton ]
+        mainWindow#testLocalHttpDaemonButton; mainWindow#testBrokerButton ]
 
     method private initGui =
 
         (* GUI: main window *)
-      let on_exit =
-        match on_exit with
-        | None -> (fun () -> self#quit (); false)
-        | Some f -> (fun () -> f (); true)
-      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;
@@ -128,8 +125,6 @@ class hbugsClient
         (* GUI: client registration *)
       ignore (mainWindow#registerClientButton#connect#clicked
         self#registerToBroker);
-      ignore (mainWindow#unregisterClientButton#connect#clicked
-        self#unregisterFromBroker);
 
         (* GUI: subscriptions *)
       ignore (mainWindow#showSubscriptionWindowButton#connect#clicked
@@ -142,7 +137,9 @@ 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)
+          | Some event ->
+              describe_hint_callback (self#hint row)
           | _ -> ()));
 
         (* GUI: main status bar *)
@@ -157,7 +154,10 @@ class hbugsClient
       let tutor_id_of_row row = subscribeWindow#tutorsCList#cell_text row 0 in
       ignore (subscribeWindow#tutorsCList#connect#select_row
         (fun ~row ~column ~event ->
-          selectedTutors <- tutor_id_of_row row :: selectedTutors));
+          let new_id = tutor_id_of_row row in
+          match selectedTutors with
+          | hd :: _ when hd = new_id -> ()  (* avoid double select events *)
+          | _ -> selectedTutors <- tutor_id_of_row row :: selectedTutors));
       ignore (subscribeWindow#tutorsCList#connect#unselect_row
         (fun ~row ~column ~event ->
           selectedTutors <-
@@ -166,6 +166,7 @@ class hbugsClient
         self#subscribeSelected);
       ignore (subscribeWindow#subscribeAllButton#connect#clicked
         self#subscribeAll);
+      subscribeWindow#tutorsCList#set_column ~visibility:false 0;
       let ctxt = subscribeWindow#subscribeWindowStatusBar#new_context "0" in
       subscribeWindowStatusContext <- Some ctxt;
       ignore (ctxt#push "Ready");
@@ -312,14 +313,12 @@ Error: %s"
                   (Hbugs_messages.string_of_msg unexpected_msg)))
 
     method registerToBroker () =
+      (match brokerId with  (* undo previous registration, if any *)
+      | Some id -> self#unregisterFromBroker ()
+      | _ -> ());
       self#sendReq ~msg:(Register_client (myOwnId, myOwnUrl))
         (function
-          | Client_registered broker_id ->
-              brokerId <- Some broker_id;
-(*
-              self#showDialog
-                (sprintf "Client %s registered @ broker %s" myOwnId broker_id)
-*)
+          | Client_registered broker_id -> (brokerId <- Some broker_id)
           | unexpected_msg ->
               self#showDialog
                 (sprintf "Client NOT registered, unexpected message:\n%s"
@@ -327,15 +326,22 @@ Error: %s"
 
     method unregisterFromBroker () =
       self#sendReq ~wait:true ~msg:(Unregister_client myOwnId)
-        self#showMsgInDialog
+        (function
+          | Client_unregistered _ -> (brokerId <- None)
+          | unexpected_msg -> ())
+(*
+              self#showDialog
+                (sprintf "Client NOT unregistered, unexpected message:\n%s"
+                  (Hbugs_messages.string_of_msg unexpected_msg)))
+*)
 
     method stateChange new_state =
+      mainWindow#hintsCList#clear ();
+      hints <- [];
       self#sendReq
         ~msg:(State_change (myOwnId, new_state))
         (function
-          | State_accepted _ ->
-              mainWindow#hintsCList#clear ();
-              hints <- []
+          | State_accepted _ -> ()
           | unexpected_msg ->
               self#showDialog
                 (sprintf "State NOT accepted by Hbugs, unexpected message:\n%s"
@@ -396,7 +402,7 @@ Error: %s"
 
     method private quit () =
       self#unregisterFromBroker ();
-      GMain.Main.quit ()
+      destroy_callback ()
 
       (** enable/disable debugging *)
     method private setDebug value = debug <- value