From: Stefano Zacchiroli Date: Mon, 25 Jul 2005 10:15:36 +0000 (+0000) Subject: handle multiple href X-Git-Tag: V_0_7_2~90 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84c9131c30a4a991c595f61620794b1b75a5a16d;p=helm.git handle multiple href --- diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 56abbf0b0..b9affc236 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -66,6 +66,13 @@ let increase_font_size () = incr current_font_size let decrease_font_size () = decr current_font_size let reset_font_size () = current_font_size := default_font_size () + (* is there any lablgtk2 constant corresponding to the left mouse button??? *) +let left_button = 1 + +let near (x1, y1) (x2, y2) = + let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in + (distance < 4.) + class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in @@ -78,9 +85,11 @@ class clickableMathView obj = initializer self#set_font_size !current_font_size; ignore (self#connect#selection_changed self#choose_selection); - ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + ignore (self#event#connect#button_press self#button_press); + ignore (self#event#connect#button_release self#button_release); +(* ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with - | Some elt (* element is an hyperlink, use href_callback on it *) + | Some elt |+ element is an hyperlink, use href_callback on it +| when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () @@ -90,7 +99,57 @@ class clickableMathView obj = in f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) - | None -> ())) + | 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) + method private choose_selection gdome_elt = let rec aux elt = if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then @@ -167,11 +226,9 @@ class sequentViewer obj = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); -(* let name = "sequent_viewer.xml" in prerr_endline ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); -*) self#load_root ~root:mathml#get_documentElement end