uniform use of Document_View.robust_body;
authorwenzelm
Wed Jun 15 21:11:53 2011 +0200 (2011-06-15 ago)
changeset 43404c8369f3d88a1
parent 43403 c2b0cfeaa5ab
child 43405 723a8af9d3f0
uniform use of Document_View.robust_body;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:30:03 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 21:11:53 2011 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4  import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
     1.5  import javax.swing.event.{CaretListener, CaretEvent}
     1.6  
     1.7 +import org.gjt.sp.util.Log
     1.8 +
     1.9  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    1.10  import org.gjt.sp.jedit.gui.RolloverButton
    1.11  import org.gjt.sp.jedit.options.GutterOptionPane
    1.12 @@ -67,6 +69,20 @@
    1.13    private val session = model.session
    1.14  
    1.15  
    1.16 +  /** robust extension body **/
    1.17 +
    1.18 +  def robust_body[A](default: A)(body: => A): A =
    1.19 +    Swing_Thread.now {
    1.20 +      try {
    1.21 +        Isabelle.buffer_lock(model.buffer) {
    1.22 +          if (model.buffer == text_area.getBuffer) body
    1.23 +          else default
    1.24 +        }
    1.25 +      }
    1.26 +      catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    1.27 +    }
    1.28 +
    1.29 +
    1.30    /** token handling **/
    1.31  
    1.32    /* visible line ranges */
    1.33 @@ -198,7 +214,7 @@
    1.34    {
    1.35      override def getToolTipText(x: Int, y: Int): String =
    1.36      {
    1.37 -      Isabelle.swing_buffer_lock(model.buffer) {
    1.38 +      robust_body(null: String) {
    1.39          val snapshot = model.snapshot()
    1.40          val offset = text_area.xyToOffset(x, y)
    1.41          if (control) {
    1.42 @@ -226,30 +242,32 @@
    1.43        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.44        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.45      {
    1.46 -      val gutter = text_area.getGutter
    1.47 -      val width = GutterOptionPane.getSelectionAreaWidth
    1.48 -      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    1.49 -      val FOLD_MARKER_SIZE = 12
    1.50 -
    1.51 -      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.52 -        Isabelle.swing_buffer_lock(model.buffer) {
    1.53 -          val snapshot = model.snapshot()
    1.54 -          for (i <- 0 until physical_lines.length) {
    1.55 -            if (physical_lines(i) != -1) {
    1.56 -              val line_range = proper_line_range(start(i), end(i))
    1.57 -
    1.58 -              // gutter icons
    1.59 -              val icons =
    1.60 -                (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
    1.61 -                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
    1.62 -                yield icon).toList.sortWith(_ >= _)
    1.63 -              icons match {
    1.64 -                case icon :: _ =>
    1.65 -                  val icn = icon.icon
    1.66 -                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
    1.67 -                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
    1.68 -                  icn.paintIcon(gutter, gfx, x0, y0)
    1.69 -                case Nil =>
    1.70 +      robust_body(()) {
    1.71 +        val gutter = text_area.getGutter
    1.72 +        val width = GutterOptionPane.getSelectionAreaWidth
    1.73 +        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    1.74 +        val FOLD_MARKER_SIZE = 12
    1.75 +  
    1.76 +        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.77 +          Isabelle.swing_buffer_lock(model.buffer) {
    1.78 +            val snapshot = model.snapshot()
    1.79 +            for (i <- 0 until physical_lines.length) {
    1.80 +              if (physical_lines(i) != -1) {
    1.81 +                val line_range = proper_line_range(start(i), end(i))
    1.82 +  
    1.83 +                // gutter icons
    1.84 +                val icons =
    1.85 +                  (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
    1.86 +                    snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
    1.87 +                  yield icon).toList.sortWith(_ >= _)
    1.88 +                icons match {
    1.89 +                  case icon :: _ =>
    1.90 +                    val icn = icon.icon
    1.91 +                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
    1.92 +                    val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
    1.93 +                    icn.paintIcon(gutter, gfx, x0, y0)
    1.94 +                  case Nil =>
    1.95 +                }
    1.96                }
    1.97              }
    1.98            }
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:30:03 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 21:11:53 2011 +0200
     2.3 @@ -14,8 +14,6 @@
     2.4  import java.text.AttributedString
     2.5  import java.util.ArrayList
     2.6  
     2.7 -import org.gjt.sp.util.Log
     2.8 -
     2.9  import org.gjt.sp.jedit.Debug
    2.10  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    2.11  import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
    2.12 @@ -27,15 +25,6 @@
    2.13    private val buffer = model.buffer
    2.14    private val text_area = doc_view.text_area
    2.15  
    2.16 -  private def painter_body(body: => Unit)
    2.17 -  {
    2.18 -    if (buffer == text_area.getBuffer)
    2.19 -      Swing_Thread.now {
    2.20 -        try { Isabelle.buffer_lock(buffer) { body } }
    2.21 -        catch { case t: Throwable => Log.log(Log.ERROR, this, t) }
    2.22 -      }
    2.23 -  }
    2.24 -
    2.25  
    2.26    /* original painters */
    2.27  
    2.28 @@ -63,8 +52,10 @@
    2.29        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.30        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.31      {
    2.32 -      painter_snapshot = model.snapshot()
    2.33 -      painter_clip = gfx.getClip
    2.34 +      doc_view.robust_body(()) {
    2.35 +        painter_snapshot = model.snapshot()
    2.36 +        painter_clip = gfx.getClip
    2.37 +      }
    2.38      }
    2.39    }
    2.40  
    2.41 @@ -74,8 +65,10 @@
    2.42        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.43        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.44      {
    2.45 -      painter_snapshot = null
    2.46 -      painter_clip = null
    2.47 +      doc_view.robust_body(()) {
    2.48 +        painter_snapshot = null
    2.49 +        painter_clip = null
    2.50 +      }
    2.51      }
    2.52    }
    2.53  
    2.54 @@ -88,7 +81,7 @@
    2.55        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.56        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.57      {
    2.58 -      painter_body {
    2.59 +      doc_view.robust_body(()) {
    2.60          val snapshot = painter_snapshot
    2.61          val ascent = text_area.getPainter.getFontMetrics.getAscent
    2.62  
    2.63 @@ -268,7 +261,7 @@
    2.64        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.65        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.66      {
    2.67 -      painter_body {
    2.68 +      doc_view.robust_body(()) {
    2.69          val clip = gfx.getClip
    2.70          val x0 = text_area.getHorizontalOffset
    2.71          val fm = text_area.getPainter.getFontMetrics
    2.72 @@ -308,8 +301,10 @@
    2.73      override def paintValidLine(gfx: Graphics2D,
    2.74        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    2.75      {
    2.76 -      if (before) gfx.clipRect(0, 0, 0, 0)
    2.77 -      else gfx.setClip(painter_clip)
    2.78 +      doc_view.robust_body(()) {
    2.79 +        if (before) gfx.clipRect(0, 0, 0, 0)
    2.80 +        else gfx.setClip(painter_clip)
    2.81 +      }
    2.82      }
    2.83    }
    2.84  
    2.85 @@ -323,7 +318,7 @@
    2.86      override def paintValidLine(gfx: Graphics2D,
    2.87        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    2.88      {
    2.89 -      painter_body {
    2.90 +      doc_view.robust_body(()) {
    2.91          if (text_area.hasFocus) {
    2.92            val caret = text_area.getCaretPosition
    2.93            if (start <= caret && caret == end - 1) {