From: Stefano Zacchiroli 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 ();