# HG changeset patch
# User wenzelm
# Date 1308165113 -7200
# Node ID c8369f3d88a15e9486ca1875f45b779d20a53f2a
# Parent  c2b0cfeaa5abf72fe83362c346ea08f4f32576fb
uniform use of Document_View.robust_body;

diff -r c2b0cfeaa5ab -r c8369f3d88a1 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:30:03 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 21:11:53 2011 +0200
@@ -18,6 +18,8 @@
 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
 import javax.swing.event.{CaretListener, CaretEvent}
 
+import org.gjt.sp.util.Log
+
 import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
@@ -67,6 +69,20 @@
   private val session = model.session
 
 
+  /** robust extension body **/
+
+  def robust_body[A](default: A)(body: => A): A =
+    Swing_Thread.now {
+      try {
+        Isabelle.buffer_lock(model.buffer) {
+          if (model.buffer == text_area.getBuffer) body
+          else default
+        }
+      }
+      catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+    }
+
+
   /** token handling **/
 
   /* visible line ranges */
@@ -198,7 +214,7 @@
   {
     override def getToolTipText(x: Int, y: Int): String =
     {
-      Isabelle.swing_buffer_lock(model.buffer) {
+      robust_body(null: String) {
         val snapshot = model.snapshot()
         val offset = text_area.xyToOffset(x, y)
         if (control) {
@@ -226,30 +242,32 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      val gutter = text_area.getGutter
-      val width = GutterOptionPane.getSelectionAreaWidth
-      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
-      val FOLD_MARKER_SIZE = 12
-
-      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
-        Isabelle.swing_buffer_lock(model.buffer) {
-          val snapshot = model.snapshot()
-          for (i <- 0 until physical_lines.length) {
-            if (physical_lines(i) != -1) {
-              val line_range = proper_line_range(start(i), end(i))
-
-              // gutter icons
-              val icons =
-                (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
-                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
-                yield icon).toList.sortWith(_ >= _)
-              icons match {
-                case icon :: _ =>
-                  val icn = icon.icon
-                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
-                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
-                  icn.paintIcon(gutter, gfx, x0, y0)
-                case Nil =>
+      robust_body(()) {
+        val gutter = text_area.getGutter
+        val width = GutterOptionPane.getSelectionAreaWidth
+        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
+        val FOLD_MARKER_SIZE = 12
+  
+        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
+          Isabelle.swing_buffer_lock(model.buffer) {
+            val snapshot = model.snapshot()
+            for (i <- 0 until physical_lines.length) {
+              if (physical_lines(i) != -1) {
+                val line_range = proper_line_range(start(i), end(i))
+  
+                // gutter icons
+                val icons =
+                  (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
+                    snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+                  yield icon).toList.sortWith(_ >= _)
+                icons match {
+                  case icon :: _ =>
+                    val icn = icon.icon
+                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
+                    val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
+                    icn.paintIcon(gutter, gfx, x0, y0)
+                  case Nil =>
+                }
               }
             }
           }
diff -r c2b0cfeaa5ab -r c8369f3d88a1 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) {