even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);

--- 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)
       }