author | wenzelm |
Thu, 22 Nov 2012 14:53:02 +0100 | |
changeset 50165 | 24d47733975f |
parent 50164 | 77668b522ffe |
child 50166 | 2585c81d840a |
--- 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 }