--- 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 =>
+ }
}
}
}
--- 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) {