From: Claudio Sacerdoti Coen Date: Tue, 1 Jul 2003 09:16:51 +0000 (+0000) Subject: 1. freeze/thaw added to reduce flickering due to selection changes X-Git-Tag: camera_ready~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=93393088bc8d331fb1cb0a81d94074240b16df4d 1. freeze/thaw added to reduce flickering due to selection changes 2. SEMANTICA CHANGE: structural selection is no longer activated just before semantic selection --- diff --git a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml index ba12fdfdf..928e21965 100644 --- a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml +++ b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml @@ -41,7 +41,7 @@ let same_element (e1 : Gdome.element option) (e2 : Gdome.element option) = 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 @@ -74,7 +74,8 @@ let mem (el : Gdome.element) = let remove (el : Gdome.element) = let rec remove_aux = function - hd::tl when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) -> remove_aux tl + hd::tl when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) -> + remove_aux tl | hd::tl -> hd::(remove_aux tl) | [] -> [] in @@ -95,25 +96,33 @@ class single_selection_math_view obj = val mutable selection_changed = (fun _ -> ()) method set_selection elem = + self#freeze ; begin match root_selected with None -> () | Some e -> self#unselect e end; - root_selected <- elem; - match elem with - None -> () - | Some e -> self#select e + root_selected <- elem ; + begin + match elem with + None -> () + | Some e -> self#select e + end ; + self#thaw method get_selection = root_selected method connect = - new single_selection_math_view_signals obj (function f -> selection_changed <- f) + new + single_selection_math_view_signals obj + (function f -> selection_changed <- f) method action_toggle (elem : Gdome.element) = match elem#get_namespaceURI, elem#get_localName with - Some ns, Some ln when ns#to_string = "http://www.w3.org/1998/Math/MathML" && - ln#to_string = "maction" -> + Some ns, Some ln + when ns#to_string = "http://www.w3.org/1998/Math/MathML" && + ln#to_string = "maction" + -> begin let selection_attr = Gdome.domString "selection" in let selection = @@ -124,10 +133,11 @@ class single_selection_math_view obj = in self#freeze ; (* the widget will cast the index back into a valid range *) - elem#setAttribute ~name:selection_attr ~value:(Gdome.domString (string_of_int (selection + 1))) ; + elem#setAttribute ~name:selection_attr + ~value:(Gdome.domString (string_of_int (selection + 1))) ; self#thaw ; true - end + end | _ -> begin match elem#get_parentNode with @@ -139,18 +149,16 @@ class single_selection_math_view obj = GdomeInit.DOMCastException _ -> false end | None -> assert false (* every element has a parent *) - end + end initializer + selection_changed <- self#set_selection ; + ignore (self#connect#select_begin (fun (elem : Gdome.element option) _ -> - if not (same_element root_selected elem) then - begin - self#set_selection elem ; - selection_changed elem - end ; - first_selected <- elem)) ; + if not (same_element root_selected elem) then selection_changed elem ; + first_selected <- elem)) ; ignore (self#connect#select_over @@ -158,15 +166,14 @@ class single_selection_math_view obj = 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)))) + (Some + (new Gdome.element_of_node + (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node)))) | _ -> None - in + in if not (same_element root_selected new_selected) then - begin - self#set_selection new_selected ; - selection_changed new_selected - end)) ; - + selection_changed new_selected)) ; + ignore (self#connect#select_end (fun (elem : Gdome.element option) _ -> first_selected <- None)) ; @@ -175,9 +182,9 @@ class single_selection_math_view obj = (self#connect#select_abort (fun () -> first_selected <- None ; - selection_changed None)) ; + selection_changed None)) ; - ignore (self#connect#click (fun _ _ -> self#set_selection None)) + ignore (self#connect#click (fun _ _ -> self#set_selection None)) end ;; @@ -190,21 +197,25 @@ let single_selection_math_view ?adjustmenth ?adjustmentv ?font_size ?font_manage () in GtkBase.Container.set w ?border_width ?width ?height; - let mathview = GObj.pack_return (new single_selection_math_view w) ~packing ~show in - begin - match font_size with - | Some size -> mathview#set_font_size size - | None -> () - end; - begin - match font_manager with - | Some manager -> mathview#set_font_manager_type ~fm_type:manager - | None -> () - end; - mathview + let mathview = + GObj.pack_return (new single_selection_math_view w) ~packing ~show + in + begin + match font_size with + | Some size -> mathview#set_font_size size + | None -> () + end; + begin + match font_manager with + | Some manager -> mathview#set_font_manager_type ~fm_type:manager + | None -> () + end; + mathview ;; -class multi_selection_math_view_signals obj (set_selection_changed : (Gdome.element option -> unit) -> unit) = +class multi_selection_math_view_signals obj + (set_selection_changed : (Gdome.element option -> unit) -> unit) += object inherit GMathView.math_view_signals obj method selection_changed = set_selection_changed @@ -222,11 +233,15 @@ class multi_selection_math_view obj = self#unselect elem method remove_selections = + self#freeze ; List.iter (fun e -> self#unselect e) selected ; selected <- [] ; - match self#get_selection with - None -> () - | Some e -> self#select e + begin + match self#get_selection with + None -> () + | Some e -> self#select e + end ; + self#thaw method add_selection (elem : Gdome.element) = selected <- elem::(remove_descendants_of elem selected) ; @@ -235,47 +250,53 @@ class multi_selection_math_view obj = method get_selections = selected method set_selection elem = + self#freeze ; begin match root_selected with None -> () | Some e -> self#unselect e ; List.iter (fun e -> self#select e) selected end; root_selected <- elem; - match elem with - None -> () - | Some e -> self#select e + begin + match elem with + None -> () + | Some e -> self#select e + end ; + self#thaw initializer ignore (self#connect#select_begin (fun _ state -> - if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then self#remove_selections)) ; + if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then + self#remove_selections)) ; ignore (self#connect#select_over (fun _ state -> Printf.printf "stable selections: %d\n" (List.length selected) ; Printf.printf "select_over with state: " ; - let c = - function - `SHIFT -> "shift " - | `LOCK -> "lock " - | `CONTROL -> "control " - | `MOD1 -> "mod1 " - | _ -> "" - in - List.iter (fun x -> print_string (c x)) (Gdk.Convert.modifier state) ; - print_char '\n' ; - flush stdout)) ; + let c = + function + `SHIFT -> "shift " + | `LOCK -> "lock " + | `CONTROL -> "control " + | `MOD1 -> "mod1 " + | _ -> "" + in + List.iter (fun x -> print_string (c x)) (Gdk.Convert.modifier state) ; + print_char '\n' ; + flush stdout)) ; ignore (self#connect#select_end (fun _ state -> Printf.printf "select_end\n" ; flush stdout ; - 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)) ; + 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)) ; ignore (self#connect#click