# HG changeset patch
# User wenzelm
# Date 1353592382 -3600
# Node ID 24d47733975f683c0946fdfa74752d6d8433e91c
# Parent  77668b522ffeaceff6d7771dda5f30482220b6df
reset active area for outdated snapshot (again?);

diff -r 77668b522ffe -r 24d47733975f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 22 14:40:39 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 22 14:53:02 2012 +0100
@@ -179,7 +179,7 @@
                 val rendering = get_rendering()
                 for ((area, require_control) <- active_areas)
                 {
-                  if (control == require_control)
+                  if (control == require_control && !rendering.snapshot.is_outdated)
                     area.update_rendering(rendering, range)
                   else area.reset
                 }