1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:30:03 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 21:11:53 2011 +0200
     1.3 @@ -14,8 +14,6 @@
     1.4  import java.text.AttributedString
     1.5  import java.util.ArrayList
     1.6  
     1.7 -import org.gjt.sp.util.Log
     1.8 -
     1.9  import org.gjt.sp.jedit.Debug
    1.10  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    1.11  import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
    1.12 @@ -27,15 +25,6 @@
    1.13    private val buffer = model.buffer
    1.14    private val text_area = doc_view.text_area
    1.15  
    1.16 -  private def painter_body(body: => Unit)
    1.17 -  {
    1.18 -    if (buffer == text_area.getBuffer)
    1.19 -      Swing_Thread.now {
    1.20 -        try { Isabelle.buffer_lock(buffer) { body } }
    1.21 -        catch { case t: Throwable => Log.log(Log.ERROR, this, t) }
    1.22 -      }
    1.23 -  }
    1.24 -
    1.25  
    1.26    /* original painters */
    1.27  
    1.28 @@ -63,8 +52,10 @@
    1.29        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.30        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.31      {
    1.32 -      painter_snapshot = model.snapshot()
    1.33 -      painter_clip = gfx.getClip
    1.34 +      doc_view.robust_body(()) {
    1.35 +        painter_snapshot = model.snapshot()
    1.36 +        painter_clip = gfx.getClip
    1.37 +      }
    1.38      }
    1.39    }
    1.40  
    1.41 @@ -74,8 +65,10 @@
    1.42        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.43        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.44      {
    1.45 -      painter_snapshot = null
    1.46 -      painter_clip = null
    1.47 +      doc_view.robust_body(()) {
    1.48 +        painter_snapshot = null
    1.49 +        painter_clip = null
    1.50 +      }
    1.51      }
    1.52    }
    1.53  
    1.54 @@ -88,7 +81,7 @@
    1.55        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.56        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.57      {
    1.58 -      painter_body {
    1.59 +      doc_view.robust_body(()) {
    1.60          val snapshot = painter_snapshot
    1.61          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.62  
    1.63 @@ -268,7 +261,7 @@
    1.64        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.65        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.66      {
    1.67 -      painter_body {
    1.68 +      doc_view.robust_body(()) {
    1.69          val clip = gfx.getClip
    1.70          val x0 = text_area.getHorizontalOffset
    1.71          val fm = text_area.getPainter.getFontMetrics
    1.72 @@ -308,8 +301,10 @@
    1.73      override def paintValidLine(gfx: Graphics2D,
    1.74        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    1.75      {
    1.76 -      if (before) gfx.clipRect(0, 0, 0, 0)
    1.77 -      else gfx.setClip(painter_clip)
    1.78 +      doc_view.robust_body(()) {
    1.79 +        if (before) gfx.clipRect(0, 0, 0, 0)
    1.80 +        else gfx.setClip(painter_clip)
    1.81 +      }
    1.82      }
    1.83    }
    1.84  
    1.85 @@ -323,7 +318,7 @@
    1.86      override def paintValidLine(gfx: Graphics2D,
    1.87        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    1.88      {
    1.89 -      painter_body {
    1.90 +      doc_view.robust_body(()) {
    1.91          if (text_area.hasFocus) {
    1.92            val caret = text_area.getCaretPosition
    1.93            if (start <= caret && caret == end - 1) {