# HG changeset patch
# User wenzelm
# Date 1407174445 -7200
# Node ID 4d86378e635ff69bee200e0a0e846fc37261c108
# Parent  73c683e09401f4c9d8c3ddb189b7d309e3b4a046
even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);

diff -r 73c683e09401 -r 4d86378e635f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 04 17:55:11 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 04 19:47:25 2014 +0200
@@ -205,6 +205,7 @@
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseDragged(evt: MouseEvent) {
       robust_body(()) {
+        active_reset()
         Completion_Popup.Text_Area.dismissed(text_area)
         Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
       }