From: Luca Padovani <luca.padovani@unito.it>
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
  ;;