X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fclient%2Fhbugs_client.ml;h=4613dbf0d57ddeabe071b299d1576c30cb6cf052;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=8eac8a022c8ec9f679ec59f5823aed6d2859535c;hpb=a8f79e24d38d0868e2ab64428ed43ed7e52f459d;p=helm.git

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