# HG changeset patch
# User wenzelm
# Date 1461612743 -7200
# Node ID 9478f0dff636cbd3b703cde4ca3be0f2fcccd3b6
# Parent  df83a961d3a82880fafc16ef6a304873507e677d
clarified rendering;

diff -r df83a961d3a8 -r 9478f0dff636 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Apr 25 19:41:39 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Apr 25 21:32:23 2016 +0200
@@ -86,7 +86,7 @@
       painter_clip = gfx.getClip
       caret_focus =
         JEdit_Lib.visible_range(text_area) match {
-          case Some(visible_range) if caret_enabled =>
+          case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated =>
             painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
           case _ => Set.empty[Long]
         }