+ | None -> ())) *)
+
+ val mutable button_press_x = -1.
+ val mutable button_press_y = -1.
+
+ method private button_press gdk_button =
+ button_press_x <- GdkEvent.Button.x gdk_button;
+ button_press_y <- GdkEvent.Button.y gdk_button;
+ false
+
+ method private button_release gdk_button =
+ let button_release_x = GdkEvent.Button.x gdk_button in
+ let button_release_y = GdkEvent.Button.y gdk_button in
+ (if near (button_press_x, button_press_y)
+ (button_release_x, button_release_y)
+ then
+ let x = int_of_float button_press_x in
+ let y = int_of_float button_press_y in
+ (match self#get_element_at x y with
+ | None -> ()
+ | Some elt ->
+ let namespaceURI = DomMisc.xlink_ns in
+ let localName = href in
+ if elt#hasAttributeNS ~namespaceURI ~localName then
+ self#invoke_href_callback
+ (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+ gdk_button
+ else
+ ignore (self#action_toggle elt)));
+ false
+
+ method private invoke_href_callback href_value gdk_button =
+ let button = GdkEvent.Button.button gdk_button in
+ if button = left_button then
+ let time = GdkEvent.Button.time gdk_button in
+ match href_callback with
+ | None -> ()
+ | Some f ->
+ (match MatitaMisc.split href_value with
+ | [ uri ] -> f uri
+ | uris ->
+ let menu = GMenu.menu () in
+ List.iter
+ (fun uri ->
+ let menu_item =
+ GMenu.menu_item ~label:uri ~packing:menu#append ()
+ in
+ ignore (menu_item#connect#activate (fun () -> f uri)))
+ uris;
+ menu#popup ~button ~time)
+