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