1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 00:10:39 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 13:55:53 2011 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     1.5      {
     1.6        doc_view.robust_body(()) {
     1.7 -        painter_snapshot = model.snapshot()
     1.8 +        painter_snapshot = doc_view.update_snapshot()
     1.9          painter_clip = gfx.getClip
    1.10        }
    1.11      }