From e02d9ce6273a9c4b91327e4fdb32100f9cbe3ff6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 7 Nov 2003 11:04:17 +0000 Subject: [PATCH] Porting to lablgtk2 completed. --- helm/hbugs/client/hbugs_client.ml | 35 +++++++++++++++++-------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml index 8eac8a022..4613dbf0d 100644 --- a/helm/hbugs/client/hbugs_client.ml +++ b/helm/hbugs/client/hbugs_client.ml @@ -225,23 +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#selection#set_select_function - (fun path already_selected -> - let row = -prerr_endline ("**** BEFORE CRASH: " ^ if already_selected then "yes" else "no") ; - match GTree.Path.get_indices path with - [|n|] -> n - | _ -> assert false - in -prerr_endline ("**** AFTER CRASH: " ^ string_of_int row) ; - (*CSC: there used to be an event whose type was checked against *) - (*CSC: `TWO_BUTTON_PRESS. This is just a bad approximation. *) - if already_selected then - use_hint_callback (self#hint row) - else - describe_hint_callback (self#hint row) ; - true)) ; + 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 -- 2.39.2