X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fclient%2Fhbugs_client.ml;h=1cab49c7609e361e7de3c52c9e498d941eafc443;hb=fde0ad77237a2fbdfb5621d5b5085fe7c82e3f92;hp=d9512d26cfcbf732dc7ec2ab194837fdf58d0a2a;hpb=39559db1a359271e8794fe8e08c21afe73a581d9;p=helm.git

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index d9512d26c..1cab49c76 100644
--- a/helm/hbugs/client/hbugs_client.ml
+++ b/helm/hbugs/client/hbugs_client.ml
@@ -32,16 +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
-  ?(use_hint_callback: hint -> unit = (fun _ -> ()))
+  ?(use_hint_callback: hint -> unit = do_nothing)
+  ?(describe_hint_callback: hint -> unit = do_nothing)
+  ?(destroy_callback: unit -> unit = do_nothing)
   ()
   =
 
@@ -91,17 +87,19 @@ class hbugsClient
       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 = 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;
@@ -127,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,6 +138,8 @@ class hbugsClient
           match event with
           | Some event when GdkEvent.get_type event = `TWO_BUTTON_PRESS ->
               use_hint_callback (self#hint row)
+          | Some event ->
+              describe_hint_callback (self#hint row)
           | _ -> ()));
 
         (* GUI: main status bar *)
@@ -156,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 <-
@@ -165,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");
@@ -311,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"
@@ -326,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"
@@ -395,7 +402,7 @@ Error: %s"
 
     method private quit () =
       self#unregisterFromBroker ();
-      GMain.Main.quit ()
+      destroy_callback ()
 
       (** enable/disable debugging *)
     method private setDebug value = debug <- value