# HG changeset patch
# User wenzelm
# Date 1353926536 -3600
# Node ID 2a3d6d760629ea4726d037a96af68eb0fda0400e
# Parent  747db833fbf76b53b617c2b7e19cccb9dd8bf793
always reset active areas;

diff -r 747db833fbf7 -r 2a3d6d760629 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 10:37:05 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 11:42:16 2012 +0100
@@ -172,7 +172,7 @@
         if ((control || hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
             JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
-              case None =>
+              case None => active_reset()
               case Some(range) =>
                 val rendering = get_rendering()
                 for ((area, require_control) <- active_areas)