From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 28 Jul 2005 14:52:19 +0000 (+0000)
Subject: bugfix: call add_selection_target each time selection changes so that
X-Git-Tag: V_0_7_2~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e633d3673762de8bf599442f874fe0e9a88e08a;p=helm.git

bugfix: call add_selection_target each time selection changes so that
selection works more than once
---

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f81b2a226..efda8cd76 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -95,14 +95,11 @@ object (self)
     ignore (self#event#connect#button_press self#button_press_cb);
     ignore (self#event#connect#button_release self#button_release_cb);
     ignore (self#event#connect#selection_clear self#selection_clear_cb);
-    ignore (self#coerce#misc#connect#selection_get self#selection_get_cb);
-    self#coerce#misc#add_selection_target
-      ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary
+    ignore (self#coerce#misc#connect#selection_get self#selection_get_cb)
 
   val mutable button_press_x = -1.
   val mutable button_press_y = -1.
   val mutable selection_changed = false
-(*   val mutable ignore_next_selection_clear = false *)
 
   method private selection_get_cb ctxt ~info ~time =
     (match self#get_selections with
@@ -194,6 +191,8 @@ object (self)
             ~localName:xref_ds)#to_string <> "" *)
       then begin
         self#set_selection (Some elt);
+        self#coerce#misc#add_selection_target
+          ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
         ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
       end else
         try