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 f81b2a2266677b43773d606608979792a604e412..efda8cd7638e209fb4d580a9b6cf2bc9e8484e98 100644 (file)
--- 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