1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 10:37:05 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 11:42:16 2012 +0100
     1.3 @@ -172,7 +172,7 @@
     1.4          if ((control || hovering) && !buffer.isLoading) {
     1.5            JEdit_Lib.buffer_lock(buffer) {
     1.6              JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
     1.7 -              case None =>
     1.8 +              case None => active_reset()
     1.9                case Some(range) =>
    1.10                  val rendering = get_rendering()
    1.11                  for ((area, require_control) <- active_areas)