1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:22:58 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:26:09 2011 +0200
     1.3 @@ -14,6 +14,8 @@
     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 @@ -25,6 +27,15 @@
    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 @@ -77,7 +88,7 @@
    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 -      Isabelle.swing_buffer_lock(buffer) {
    1.33 +      painter_body {
    1.34          val snapshot = painter_snapshot
    1.35          val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.36  
    1.37 @@ -257,7 +268,7 @@
    1.38        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.39        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.40      {
    1.41 -      Isabelle.swing_buffer_lock(buffer) {
    1.42 +      painter_body {
    1.43          val clip = gfx.getClip
    1.44          val x0 = text_area.getHorizontalOffset
    1.45          val fm = text_area.getPainter.getFontMetrics
    1.46 @@ -312,16 +323,18 @@
    1.47      override def paintValidLine(gfx: Graphics2D,
    1.48        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    1.49      {
    1.50 -      if (text_area.hasFocus) {
    1.51 -        val caret = text_area.getCaretPosition
    1.52 -        if (start <= caret && caret == end - 1) {
    1.53 -          val painter = text_area.getPainter
    1.54 -          val fm = painter.getFontMetrics
    1.55 +      painter_body {
    1.56 +        if (text_area.hasFocus) {
    1.57 +          val caret = text_area.getCaretPosition
    1.58 +          if (start <= caret && caret == end - 1) {
    1.59 +            val painter = text_area.getPainter
    1.60 +            val fm = painter.getFontMetrics
    1.61  
    1.62 -          val offset = caret - text_area.getLineStartOffset(physical_line)
    1.63 -          val x = text_area.offsetToXY(physical_line, offset).x
    1.64 -          gfx.setColor(painter.getCaretColor)
    1.65 -          gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
    1.66 +            val offset = caret - text_area.getLineStartOffset(physical_line)
    1.67 +            val x = text_area.offsetToXY(physical_line, offset).x
    1.68 +            gfx.setColor(painter.getCaretColor)
    1.69 +            gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
    1.70 +          }
    1.71          }
    1.72        }
    1.73      }