X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fclient%2Fhbugs_client.ml;h=4613dbf0d57ddeabe071b299d1576c30cb6cf052;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=1cab49c7609e361e7de3c52c9e498d941eafc443;hpb=9327428bfb03330a8baf382fea019f320e5cc462;p=helm.git diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml index 1cab49c76..4613dbf0d 100644 --- a/helm/hbugs/client/hbugs_client.ml +++ b/helm/hbugs/client/hbugs_client.ml @@ -34,6 +34,101 @@ exception Invalid_URL of string;; let do_nothing _ = ();; +module SmartHbugs_client_gui = + struct + class ['a] oneColumnCList gtree_view ~column_type ~column_title + = + let obj = + ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in + let columns = new GTree.column_list in + let col = columns#add column_type in + let vcol = GTree.view_column ~title:column_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col]) in + let store = GTree.list_store columns in + object(self) + inherit GTree.view obj + method clear = store#clear + method append (v : 'a) = + let row = store#append () in + store#set ~row ~column:col v; + method column = col + initializer + self#set_model (Some (store :> GTree.model)) ; + ignore (self#append_column vcol) + end + + class ['a,'b] twoColumnsCList gtree_view ~column1_type ~column2_type + ~column1_title ~column2_title + = + let obj = + ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in + let columns = new GTree.column_list in + let col1 = columns#add column1_type in + let vcol1 = GTree.view_column ~title:column1_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col1]) in + let col2 = columns#add column2_type in + let vcol2 = GTree.view_column ~title:column2_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col2]) in + let store = GTree.list_store columns in + object(self) + inherit GTree.view obj + method clear = store#clear + method append (v1 : 'a) (v2 : 'b) = + let row = store#append () in + store#set ~row ~column:col1 v1; + store#set ~row ~column:col2 v2 + method column1 = col1 + method column2 = col2 + initializer + self#set_model (Some (store :> GTree.model)) ; + ignore (self#append_column vcol1) ; + ignore (self#append_column vcol2) ; + end + + class subscribeWindow () = + object(self) + inherit Hbugs_client_gui.subscribeWindow () + val mutable tutorsSmartCList = None + method tutorsSmartCList = + match tutorsSmartCList with + None -> assert false + | Some w -> w + initializer + tutorsSmartCList <- + Some + (new twoColumnsCList self#tutorsCList + ~column1_type:Gobject.Data.string ~column2_type:Gobject.Data.string + ~column1_title:"Id" ~column2_title:"Description") + end + + class hbugsMainWindow () = + object(self) + inherit Hbugs_client_gui.hbugsMainWindow () + val mutable subscriptionSmartCList = None + val mutable hintsSmartCList = None + method subscriptionSmartCList = + match subscriptionSmartCList with + None -> assert false + | Some w -> w + method hintsSmartCList = + match hintsSmartCList with + None -> assert false + | Some w -> w + initializer + subscriptionSmartCList <- + Some + (new oneColumnCList self#subscriptionCList + ~column_type:Gobject.Data.string ~column_title:"Description") + initializer + hintsSmartCList <- + Some + (new oneColumnCList self#hintsCList + ~column_type:Gobject.Data.string ~column_title:"Description") + end + + end +;; + class hbugsClient ?(use_hint_callback: hint -> unit = do_nothing) ?(describe_hint_callback: hint -> unit = do_nothing) @@ -51,8 +146,8 @@ class hbugsClient object (self) - val mainWindow = new Hbugs_client_gui.hbugsMainWindow () - val subscribeWindow = new Hbugs_client_gui.subscribeWindow () + val mainWindow = new SmartHbugs_client_gui.hbugsMainWindow () + val subscribeWindow = new SmartHbugs_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 @@ -62,8 +157,6 @@ class hbugsClient (* all available tutors, saved last time a List_tutors message was sent to broker *) val mutable availableTutors: tutor_dsc list = [] - (* id of highlighted tutors in tutor subscription window *) - val mutable selectedTutors: tutor_id list = [] val mutable statusContext = None val mutable subscribeWindowStatusContext = None val mutable debug = false (* enable/disable debugging buttons *) @@ -132,15 +225,26 @@ class hbugsClient self#listTutors (); subscribeWindow#subscribeWindow#show ())); + let get_selected_row_index () = + match mainWindow#hintsCList#selection#get_selected_rows with + [path] -> + (match GTree.Path.get_indices path with + [|n|] -> n + | _ -> assert false) + | _ -> assert false + in (* GUI: hints list *) - ignore (mainWindow#hintsCList#connect#select_row - (fun ~row ~column ~event -> - 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) - | _ -> ())); + ignore ( + let event_ops = new GObj.event_ops mainWindow#hintsCList#as_widget in + event_ops#connect#button_press + (fun event -> + if GdkEvent.get_type event = `TWO_BUTTON_PRESS then + use_hint_callback (self#hint (get_selected_row_index ())) ; + false)); + + ignore (mainWindow#hintsCList#selection#connect#changed + (fun () -> + describe_hint_callback (self#hint (get_selected_row_index ())))) ; (* GUI: main status bar *) let ctxt = mainWindow#mainWindowStatusBar#new_context "0" in @@ -148,25 +252,15 @@ class hbugsClient ignore (ctxt#push "Ready"); (* GUI: subscription window *) + subscribeWindow#tutorsCList#selection#set_mode `MULTIPLE; ignore (subscribeWindow#subscribeWindow#event#connect#delete (fun _ -> subscribeWindow#subscribeWindow#misc#hide (); true)); ignore (subscribeWindow#listTutorsButton#connect#clicked self#listTutors); - let tutor_id_of_row row = subscribeWindow#tutorsCList#cell_text row 0 in - ignore (subscribeWindow#tutorsCList#connect#select_row - (fun ~row ~column ~event -> - 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 <- - List.filter ((<>) (tutor_id_of_row row)) selectedTutors)); ignore (subscribeWindow#subscribeButton#connect#clicked self#subscribeSelected); ignore (subscribeWindow#subscribeAllButton#connect#clicked self#subscribeAll); - subscribeWindow#tutorsCList#set_column ~visibility:false 0; + (subscribeWindow#tutorsCList#get_column 0)#set_visible false; let ctxt = subscribeWindow#subscribeWindowStatusBar#new_context "0" in subscribeWindowStatusContext <- Some ctxt; ignore (ctxt#push "Ready"); @@ -248,7 +342,7 @@ Error: %s" List.iter (fun h -> (match h with Hints _ -> assert false | _ -> ()); - ignore (mainWindow#hintsCList#append [string_of_hint h])) + ignore(mainWindow#hintsSmartCList#append(string_of_hint h))) received_hints; hints <- hints @ received_hints; Hbugs_messages.respond_msg (Wow myOwnId) outchan @@ -336,7 +430,7 @@ Error: %s" *) method stateChange new_state = - mainWindow#hintsCList#clear (); + mainWindow#hintsSmartCList#clear (); hints <- []; self#sendReq ~msg:(State_change (myOwnId, new_state)) @@ -357,11 +451,10 @@ Error: %s" | Tutor_list (_, descriptions) -> availableTutors <- (* sort accordingly to tutor description *) List.sort (fun (a,b) (c,d) -> compare (b,a) (d,c)) descriptions; - selectedTutors <- []; - subscribeWindow#tutorsCList#clear (); + subscribeWindow#tutorsSmartCList#clear (); List.iter (fun (id, dsc) -> - ignore (subscribeWindow#tutorsCList#append [id; dsc])) + ignore (subscribeWindow#tutorsSmartCList#append id dsc)) availableTutors | unexpected_msg -> self#showDialog @@ -374,14 +467,14 @@ Error: %s" (function | (Subscribed (_, subscribedTutors)) as msg -> let sort = List.sort compare in - mainWindow#subscriptionCList#clear (); + mainWindow#subscriptionSmartCList#clear (); List.iter (fun tutor_id -> ignore - (mainWindow#subscriptionCList#append - [ try - List.assoc tutor_id availableTutors; - with Not_found -> assert false ])) + (mainWindow#subscriptionSmartCList#append + ( try + List.assoc tutor_id availableTutors + with Not_found -> assert false ))) tutors_id; subscribeWindow#subscribeWindow#misc#hide (); if sort subscribedTutors <> sort tutors_id then @@ -389,12 +482,22 @@ Error: %s" (sprintf "Subscription mismatch\n: %s" (Hbugs_messages.string_of_msg msg)) | unexpected_msg -> - mainWindow#subscriptionCList#clear (); + mainWindow#subscriptionSmartCList#clear (); self#showDialog (sprintf "Subscription FAILED, unexpected message:\n%s" (Hbugs_messages.string_of_msg unexpected_msg))) - method private subscribeSelected () = self#subscribe' selectedTutors + method private subscribeSelected () = + let tutorsSmartCList = subscribeWindow#tutorsSmartCList in + let selectedTutors = + List.map + (fun p -> + tutorsSmartCList#model#get + ~row:(tutorsSmartCList#model#get_iter p) + ~column:tutorsSmartCList#column1) + tutorsSmartCList#selection#get_selected_rows + in + self#subscribe' selectedTutors method subscribeAll () = self#listTutors (); (* this fills 'availableTutors' field *)