# HG changeset patch # User wenzelm # Date 1308168026 -7200 # Node ID 7e726f869de96489260cf2017ed016a082877177 # Parent 666962d17142fe965156892d0a1f3ccd20b6601e# Parent 40c67d894be461d53615c4628e9b72d39d0da93f merged diff -r 666962d17142 -r 7e726f869de9 src/Pure/System/event_bus.scala --- a/src/Pure/System/event_bus.scala Wed Jun 15 21:18:58 2011 +0200 +++ b/src/Pure/System/event_bus.scala Wed Jun 15 22:00:26 2011 +0200 @@ -20,7 +20,7 @@ def + (r: Actor): Event_Bus[Event] = { this += r; this } def += (f: Event => Unit) { - this += actor { loop { react { case x: Event => f(x) } } } + this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } } } def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } diff -r 666962d17142 -r 7e726f869de9 src/Pure/build-jars --- a/src/Pure/build-jars Wed Jun 15 21:18:58 2011 +0200 +++ b/src/Pure/build-jars Wed Jun 15 22:00:26 2011 +0200 @@ -117,18 +117,31 @@ ## main +declare -a UPDATED=() + if [ -n "$FRESH" ]; then OUTDATED=true else OUTDATED=false - for SOURCE in "${SOURCES[@]}" + for TARGET in "${TARGETS[@]}" do - [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE" - for TARGET in "${TARGETS[@]}" + [ ! -e "$TARGET" ] && OUTDATED=true + done + if [ "$OUTDATED" = false ]; then + for DEP in "${SOURCES[@]}" do - [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true + [ ! -e "$DEP" ] && fail "Missing file: $DEP" + UPDATE="" + for TARGET in "${TARGETS[@]}" + do + [ "$DEP" -nt "$TARGET" ] && { + OUTDATED=true + UPDATE=true + } + done + [ -n "$UPDATE" ] && UPDATED["${#UPDATED[@]}"]="$DEP" done - done + fi fi if [ "$OUTDATED" = true ] @@ -137,6 +150,14 @@ echo "### Building Isabelle/Scala layer ..." echo "###" + [ "${#UPDATED[@]}" -gt 0 ] && { + echo "Changed files:" + for FILE in "${UPDATED[@]}" + do + echo " $FILE" + done + } + rm -rf classes && mkdir classes "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \ fail "Failed to compile sources" diff -r 666962d17142 -r 7e726f869de9 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 21:18:58 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 22:00:26 2011 +0200 @@ -196,27 +196,26 @@ if [ "$OUTDATED" = true ] then + [ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable" + + [ -e "$ISABELLE_HOME/Admin/build" ] && \ + { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; } + + echo "###" + echo "### Building Isabelle/jEdit ..." + echo "###" + [ "${#UPDATED[@]}" -gt 0 ] && { - echo "Rebuild due changed files:" + echo "Changed files:" for FILE in "${UPDATED[@]}" do echo " $FILE" done } - [ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable" - [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" - [ -e "$ISABELLE_HOME/Admin/build" ] && \ - { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; } - - - echo "###" - echo "### Building Isabelle/jEdit ..." - echo "###" - rm -rf dist || failed mkdir -p dist dist/classes || failed diff -r 666962d17142 -r 7e726f869de9 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Jun 15 21:18:58 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 15 22:00:26 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 666962d17142 -r 7e726f869de9 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 21:18:58 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 22:00:26 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) {