always reset active areas;
authorwenzelm
Mon, 26 Nov 2012 11:42:16 +0100
changeset 50211 2a3d6d760629
parent 50210 747db833fbf7
child 50212 4fb06c22c5ec
always reset active areas;
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)