Hi Matthew, On 07/16/2011 10:31 PM, Matthew Flatt wrote: > Short answer: change pushed.
Thanks for picking this up. I see you also removed GDK_POINTER_MOTION_HINT_MASK , which means we will be again seeing more motion events than before. Please note that GDK_POINTER_MOTION_HINT_MASK is really orthogonal to GDK_POINTER_MOTION_MASK / GDK_BUTTON_MOTION_MASK . The latter selects in which cases motion events should be sent (GDK_POINTER_MOTION_MASK == always, GDK_BUTTON_MOTION_MASK == only when a mouse button is pressed). The former enables coalescing of motion events so that the application doesn't see so many of them. GDK_POINTER_MOTION_HINT_MASK by itself doesn't enable the sending of motion events. See also: http://www.linuxtopia.org/online_books/gui_toolkit_guides/gtk+_gnome_application_development/sec-gdkevent_5.html (Apology if you knew all this already). Note that this page states that if the motion events can be handled quickly (under 5 ms), then not using GDK_POINTER_MOTION_HINT_MASK may be preferable. I guess most apps don't do anything with the motion events which is probably quite fast indeed. Stephan _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
