From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sun, 7 Sep 2003 09:49:07 +0000 (+0000)
Subject: added "describe_hint_callback" invoked when a hint is selected
X-Git-Tag: v0_0_1~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9327428bfb03330a8baf382fea019f320e5cc462;p=helm.git

added "describe_hint_callback" invoked when a hint is selected
---

diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml
index 4e009322c..1cab49c76 100644
--- a/helm/hbugs/client/hbugs_client.ml
+++ b/helm/hbugs/client/hbugs_client.ml
@@ -32,18 +32,11 @@ open Printf;;
 
 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
-  @param on_exit function invoked when client is exiting (e.g. window is
-  destroyed, if it's None "self#quit" is invoked
-  *)
 class hbugsClient
   ?(use_hint_callback: hint -> unit = do_nothing)
+  ?(describe_hint_callback: hint -> unit = do_nothing)
   ?(destroy_callback: unit -> unit = do_nothing)
   ()
   =
@@ -94,8 +87,7 @@ 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 =
 
@@ -133,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
@@ -148,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 *)
@@ -162,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 <-
@@ -171,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");
@@ -317,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"
@@ -332,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"
diff --git a/helm/hbugs/client/hbugs_client.mli b/helm/hbugs/client/hbugs_client.mli
index 87e11e968..0c2e93d80 100644
--- a/helm/hbugs/client/hbugs_client.mli
+++ b/helm/hbugs/client/hbugs_client.mli
@@ -3,9 +3,16 @@ open Hbugs_types
 
 exception Invalid_URL of string
 
+  (*
+    @param use_hint_callback is called when the user double click on a hint
+    (default: do nothing)
+    @param describe_hint_callback is called when the user click on a hint
+    (default: do nothing)
+  *)
 class hbugsClient :
-  ?use_hint_callback: (hint -> unit) -> (* default = do nothing *)
-  ?destroy_callback: (unit -> unit) ->  (* default = do nothing *)
+  ?use_hint_callback: (hint -> unit) ->
+  ?describe_hint_callback: (hint -> unit) ->
+  ?destroy_callback: (unit -> unit) ->
   unit ->
     object
 
diff --git a/helm/hbugs/client/main.ml b/helm/hbugs/client/main.ml
index e694613c5..85972ace3 100644
--- a/helm/hbugs/client/main.ml
+++ b/helm/hbugs/client/main.ml
@@ -34,6 +34,9 @@ let client =
     ~use_hint_callback:
       (fun hint ->
         prerr_endline (sprintf "Using hint: %s" (string_of_hint hint)))
+    ~describe_hint_callback:
+      (fun hint ->
+        prerr_endline (sprintf "Describing hint: %s" (string_of_hint hint)))
     ()
 in
 client#show ();