src/Tools/jEdit/src/text_area_painter.scala

--- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:30:03 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 21:11:53 2011 +0200
@@ -14,8 +14,6 @@
 import java.text.AttributedString
 import java.util.ArrayList
 
-import org.gjt.sp.util.Log
-
 import org.gjt.sp.jedit.Debug
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
@@ -27,15 +25,6 @@
   private val buffer = model.buffer
   private val text_area = doc_view.text_area
 
-  private def painter_body(body: => Unit)
-  {
-    if (buffer == text_area.getBuffer)
-      Swing_Thread.now {
-        try { Isabelle.buffer_lock(buffer) { body } }
-        catch { case t: Throwable => Log.log(Log.ERROR, this, t) }
-      }
-  }
-
 
   /* original painters */
 
@@ -63,8 +52,10 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      painter_snapshot = model.snapshot()
-      painter_clip = gfx.getClip
+      doc_view.robust_body(()) {
+        painter_snapshot = model.snapshot()
+        painter_clip = gfx.getClip
+      }
     }
   }
 
@@ -74,8 +65,10 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      painter_snapshot = null
-      painter_clip = null
+      doc_view.robust_body(()) {
+        painter_snapshot = null
+        painter_clip = null
+      }
     }
   }
 
@@ -88,7 +81,7 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      painter_body {
+      doc_view.robust_body(()) {
         val snapshot = painter_snapshot
         val ascent = text_area.getPainter.getFontMetrics.getAscent
 
@@ -268,7 +261,7 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      painter_body {
+      doc_view.robust_body(()) {
         val clip = gfx.getClip
         val x0 = text_area.getHorizontalOffset
         val fm = text_area.getPainter.getFontMetrics
@@ -308,8 +301,10 @@
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
-      if (before) gfx.clipRect(0, 0, 0, 0)
-      else gfx.setClip(painter_clip)
+      doc_view.robust_body(()) {
+        if (before) gfx.clipRect(0, 0, 0, 0)
+        else gfx.setClip(painter_clip)
+      }
     }
   }
 
@@ -323,7 +318,7 @@
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
-      painter_body {
+      doc_view.robust_body(()) {
         if (text_area.hasFocus) {
           val caret = text_area.getCaretPosition
           if (start <= caret && caret == end - 1) {