From: Luca Padovani Date: Wed, 29 Jan 2003 13:19:26 +0000 (+0000) Subject: * implemented a more efficient selection to avoid flickering X-Git-Tag: V_0_0_4_1~85 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=42fa20a1eac55122a1c6b2b47511ed162212c29b;p=helm.git * implemented a more efficient selection to avoid flickering * click now unselect every selection even in multi_selection --- diff --git a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml index d23ce2d1c..4d10bf395 100644 --- a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml +++ b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml @@ -35,6 +35,12 @@ let common_ancestor (first : Gdome.node) (last : Gdome.node) = in (last_common (None,(List.rev (path first)),(List.rev (path last)))) +let same_element (e1 : Gdome.element option) (e2 : Gdome.element option) = + match e1, e2 with + None, None -> true + | Some e1, Some e2 when (e1 :> Gdome.node)#isSameNode (e2 :> Gdome.node) -> true + | _ -> false + (* true if n1 is n2 or one of n2's descendants *) let rec descendant_of (n1 : Gdome.node) (n2 : Gdome.node) = if n1#isSameNode n2 then true @@ -138,18 +144,27 @@ class single_selection_math_view obj = ignore (self#connect#select_begin (fun (elem : Gdome.element option) _ -> - if not (elem = root_selected) then selection_changed elem ; + if not (same_element root_selected elem) then + begin + self#set_selection elem ; + selection_changed elem + end ; first_selected <- elem)) ; ignore (self#connect#select_over (fun (elem : Gdome.element option) _ -> - match first_selected, elem with - None, _ - | _, None -> selection_changed None - | Some first', Some last' -> - selection_changed - (Some (new Gdome.element_of_node (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node)))))) ; + let new_selected = + match first_selected, elem with + Some first', Some last' -> + (Some (new Gdome.element_of_node (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node)))) + | _ -> None + in + if not (same_element root_selected new_selected) then + begin + self#set_selection new_selected ; + selection_changed new_selected + end)) ; ignore (self#connect#select_end @@ -259,8 +274,11 @@ class multi_selection_math_view obj = if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then self#remove_selections ; match root_selected with None -> () - | Some e -> self#set_selection None ; self#add_selection e)) + | Some e -> self#set_selection None ; self#add_selection e)) ; + ignore + (self#connect#click + (fun _ _ -> self#remove_selections)) end ;;