From 5e633d3673762de8bf599442f874fe0e9a88e08a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 28 Jul 2005 14:52:19 +0000 Subject: [PATCH] bugfix: call add_selection_target each time selection changes so that selection works more than once --- helm/matita/matitaMathView.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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 -- 2.39.2