# HG changeset patch
# User wenzelm
# Date 1398265548 -7200
# Node ID 140e6d01c481adfdd1f728da5b37c58c489ac1a5
# Parent  558afd4292554c9525265dacb56e3f1182a37b97# Parent  70cc1164fb83d325e16664119adc1cea7d31c685
merged

diff -r 558afd429255 -r 140e6d01c481 Admin/build
--- a/Admin/build	Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/build	Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
 
 ## main
 
-#workaround for scalac 2.10.2
+#FIXME workaround for scalac 2.11.0
 function stty() { :; }
 export -f stty
 
diff -r 558afd429255 -r 140e6d01c481 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/components/components.sha1	Wed Apr 23 17:05:48 2014 +0200
@@ -66,6 +66,7 @@
 207e4916336335386589c918c5e3f3dcc14698f2  scala-2.10.2.tar.gz
 21c8ee274ffa471ab54d4196ecd827bf3d43e591  scala-2.10.3.tar.gz
 d4688ddaf83037ca43b5bf271325fc53ae70e3aa  scala-2.10.4.tar.gz
+44d12297a78988ffd34363535e6a8e0d94c1d8b5  scala-2.11.0.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
diff -r 558afd429255 -r 140e6d01c481 Admin/components/main
--- a/Admin/components/main	Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/components/main	Wed Apr 23 17:05:48 2014 +0200
@@ -9,7 +9,7 @@
 jortho-1.0-2
 kodkodi-1.5.2
 polyml-5.5.1-1
-scala-2.10.4
+scala-2.11.0
 spass-3.8ds
 z3-3.2-1
 z3-4.3.0
diff -r 558afd429255 -r 140e6d01c481 etc/settings
--- a/etc/settings	Wed Apr 23 11:29:39 2014 +0200
+++ b/etc/settings	Wed Apr 23 17:05:48 2014 +0200
@@ -12,16 +12,11 @@
 ### Isabelle/Scala
 ###
 
-ISABELLE_SCALA_BUILD_OPTIONS="-nowarn -target:jvm-1.5 -Xmax-classfile-name 130"
+ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-library.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-swing.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-actors.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-compiler.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-reflect.jar"
 
 #paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
diff -r 558afd429255 -r 140e6d01c481 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Concurrent/future.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -2,30 +2,27 @@
     Module:     PIDE
     Author:     Makarius
 
-Future values.
-
-Notable differences to scala.actors.Future (as of Scala 2.7.7):
-
-  * We capture/release exceptions as in the ML variant.
-
-  * Future.join works for *any* actor, not just the one of the
-    original fork.
+Value-oriented parallelism via futures and promises in Scala -- with
+signatures as in Isabelle/ML.
 */
 
 package isabelle
 
 
-import scala.actors.Actor._
+import scala.util.{Success, Failure}
+import scala.concurrent.{Future => Scala_Future, Promise => Scala_Promise, Await}
+import scala.concurrent.duration.Duration
+import scala.concurrent.ExecutionContext.Implicits.global
 
 
 object Future
 {
   def value[A](x: A): Future[A] = new Finished_Future(x)
-  def fork[A](body: => A): Future[A] = new Pending_Future(body)
-  def promise[A]: Promise[A] = new Promise_Future
+  def fork[A](body: => A): Future[A] = new Pending_Future(Scala_Future[A](body))
+  def promise[A]: Promise[A] = new Promise_Future[A](Scala_Promise[A])
 }
 
-abstract class Future[A]
+trait Future[A]
 {
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
@@ -41,71 +38,43 @@
     }
 }
 
-abstract class Promise[A] extends Future[A]
+trait Promise[A] extends Future[A]
 {
   def fulfill_result(res: Exn.Result[A]): Unit
-  def fulfill(x: A) { fulfill_result(Exn.Res(x)) }
+  def fulfill(x: A): Unit
 }
 
+
 private class Finished_Future[A](x: A) extends Future[A]
 {
   val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
   val join: A = x
 }
 
-private class Pending_Future[A](body: => A) extends Future[A]
+private class Pending_Future[A](future: Scala_Future[A]) extends Future[A]
 {
-  @volatile private var result: Option[Exn.Result[A]] = None
-
-  private val evaluator = actor {
-    result = Some(Exn.capture(body))
-    loop { react { case _ => reply(result.get) } }
-  }
+  def peek: Option[Exn.Result[A]] =
+    future.value match {
+      case Some(Success(x)) => Some(Exn.Res(x))
+      case Some(Failure(e)) => Some(Exn.Exn(e))
+      case None => None
+    }
+  override def is_finished: Boolean = future.isCompleted
 
-  def peek: Option[Exn.Result[A]] = result
-
-  def join: A =
-    Exn.release {
-      peek match {
-        case Some(res) => res
-        case None => (evaluator !? ()).asInstanceOf[Exn.Result[A]]
-      }
-    }
+  def join: A = Await.result(future, Duration.Inf)
+  override def map[B](f: A => B): Future[B] = new Pending_Future[B](future.map(f))
 }
 
-private class Promise_Future[A] extends Promise[A]
+private class Promise_Future[A](promise: Scala_Promise[A])
+  extends Pending_Future(promise.future) with Promise[A]
 {
-  @volatile private var result: Option[Exn.Result[A]] = None
-
-  private case object Read
-  private case class Write(res: Exn.Result[A])
+  override def is_finished: Boolean = promise.isCompleted
 
-  private val receiver = actor {
-    loop {
-      react {
-        case Read if result.isDefined => reply(result.get)
-        case Write(res) =>
-          if (result.isDefined) reply(false)
-          else { result = Some(res); reply(true) }
-      }
+  def fulfill_result(res: Exn.Result[A]): Unit =
+    res match {
+      case Exn.Res(x) => promise.success(x)
+      case Exn.Exn(e) => promise.failure(e)
     }
-  }
-
-  def peek: Option[Exn.Result[A]] = result
-
-  def join: A =
-    Exn.release {
-      result match {
-        case Some(res) => res
-        case None => (receiver !? Read).asInstanceOf[Exn.Result[A]]
-      }
-    }
-
-  def fulfill_result(res: Exn.Result[A]) {
-    receiver !? Write(res) match {
-      case false => error("Duplicate fulfillment of promise")
-      case _ =>
-    }
-  }
+  def fulfill(x: A): Unit = promise.success(x)
 }
 
diff -r 558afd429255 -r 140e6d01c481 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -15,10 +15,10 @@
 
 object Simple_Thread
 {
-  /* prending interrupts */
+  /* pending interrupts */
 
   def interrupted_exception(): Unit =
-    if (Thread.interrupted()) throw new InterruptedException
+    if (Thread.interrupted()) throw Exn.Interrupt()
 
 
   /* plain thread */
diff -r 558afd429255 -r 140e6d01c481 src/Pure/GUI/swing_thread.scala
--- a/src/Pure/GUI/swing_thread.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/GUI/swing_thread.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -35,7 +35,7 @@
   {
     if (SwingUtilities.isEventDispatchThread()) body
     else {
-      lazy val result = { assert(); Exn.capture(body) }
+      lazy val result = { assert { Exn.capture(body) } }
       SwingUtilities.invokeAndWait(new Runnable { def run = result })
       Exn.release(result)
     }
@@ -69,7 +69,7 @@
       timer.setRepeats(false)
       timer.addActionListener(new ActionListener {
         override def actionPerformed(e: ActionEvent) {
-          assert()
+          assert {}
           timer.setInitialDelay(time.ms.toInt)
           action
         }
@@ -77,20 +77,20 @@
 
       def invoke()
       {
-        require()
+        require {}
         if (first) timer.start() else timer.restart()
       }
 
       def revoke()
       {
-        require()
+        require {}
         timer.stop()
         timer.setInitialDelay(time.ms.toInt)
       }
 
       def postpone(alt_time: Time)
       {
-        require()
+        require {}
         if (timer.isRunning) {
           timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
           timer.restart()
diff -r 558afd429255 -r 140e6d01c481 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/GUI/system_dialog.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -26,7 +26,7 @@
 
   private def check_window(): Window =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     _window match {
       case Some(window) => window
@@ -48,7 +48,7 @@
 
   private def conclude()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     require(_return_code.isDefined)
 
     _window match {
diff -r 558afd429255 -r 140e6d01c481 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -266,10 +266,10 @@
 
   /* abbreviations */
 
-  private val caret_indicator = '\007'
+  private val caret_indicator = '\u0007'
   private val antiquote = "@{"
   private val default_abbrs =
-    List("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
+    List("@{" -> "@{\u0007}", "`" -> "\\<open>\u0007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
 }
 
 final class Completion private(
diff -r 558afd429255 -r 140e6d01c481 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/exn.ML	Wed Apr 23 17:05:48 2014 +0200
@@ -19,6 +19,7 @@
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val return_code: exn -> int -> int
   val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
 end;
@@ -68,10 +69,13 @@
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
-(* POSIX process wrapper *)
+(* POSIX return code *)
+
+fun return_code exn rc =
+  if is_interrupt exn then (130: int) else rc;
 
 fun capture_exit rc f x =
-  f x handle exn => if is_interrupt exn then exit (130: int) else exit rc;
+  f x handle exn => exit (return_code exn rc);
 
 
 (* concatenated exceptions *)
diff -r 558afd429255 -r 140e6d01c481 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/exn.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -27,6 +27,34 @@
     }
 
 
+  /* interrupts */
+
+  def is_interrupt(exn: Throwable): Boolean =
+  {
+    var found_interrupt = false
+    var e = exn
+    while (!found_interrupt && e != null) {
+      found_interrupt |= e.isInstanceOf[InterruptedException]
+      e = e.getCause
+    }
+    found_interrupt
+  }
+
+  object Interrupt
+  {
+    def apply(): Throwable = new InterruptedException
+    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+
+    val return_code = 130
+  }
+
+
+  /* POSIX return code */
+
+  def return_code(exn: Throwable, rc: Int): Int =
+    if (is_interrupt(exn)) Interrupt.return_code else rc
+
+
   /* message */
 
   private val runtime_exception = Class.forName("java.lang.RuntimeException")
@@ -44,8 +72,12 @@
     else None
 
   def message(exn: Throwable): String =
-    user_message(exn) getOrElse
-      (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
-       else exn.toString)
+    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+
+
+  /* TTY error message */
+
+  def error_message(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+  def error_message(exn: Throwable): String = error_message(message(exn))
 }
 
diff -r 558afd429255 -r 140e6d01c481 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/linear_set.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -10,16 +10,18 @@
 
 
 import scala.collection.SetLike
-import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom,
-  GenericSetTemplate, GenericCompanion}
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
+import scala.collection.mutable.{Builder, SetBuilder}
+import scala.language.higherKinds
 
 
-object Linear_Set extends ImmutableSetFactory[Linear_Set]
+object Linear_Set extends SetFactory[Linear_Set]
 {
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
   override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+  def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
 
   class Duplicate[A](x: A) extends Exception
   class Undefined[A](x: A) extends Exception
diff -r 558afd429255 -r 140e6d01c481 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/scan.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -238,7 +238,7 @@
         var rest = in
         def try_parse[A](p: Parser[A]): Boolean =
         {
-          parse(p ^^^ (), rest) match {
+          parse(p ^^^ (()), rest) match {
             case Success(_, next) => { rest = next; true }
             case _ => false
           }
diff -r 558afd429255 -r 140e6d01c481 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -65,7 +65,7 @@
 
   private def content_update()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
 
     /* snapshot */
@@ -174,7 +174,7 @@
 
   def apply_query(query: List[String])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
@@ -199,7 +199,7 @@
 
   def locate_query()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     for {
       command <- current_location
diff -r 558afd429255 -r 140e6d01c481 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -88,8 +88,8 @@
         }
         catch {
           case exn: Throwable =>
-            System.err.println("Failed to initialize protocol handler: " +
-              name + "\n" + Exn.message(exn))
+            System.err.println(Exn.error_message(
+              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
             (handlers1, functions1)
         }
 
@@ -102,8 +102,8 @@
           try { functions(a)(msg) }
           catch {
             case exn: Throwable =>
-              System.err.println("Failed invocation of protocol function: " +
-                quote(a) + "\n" + Exn.message(exn))
+              System.err.println(Exn.error_message(
+                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
             false
           }
         case _ => false
diff -r 558afd429255 -r 140e6d01c481 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -16,8 +16,8 @@
 {
   /* chunk markers */
 
-  val X = '\5'
-  val Y = '\6'
+  val X = '\u0005'
+  val Y = '\u0006'
 
   val is_X = (c: Char) => c == X
   val is_Y = (c: Char) => c == Y
diff -r 558afd429255 -r 140e6d01c481 src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/command_line.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -30,8 +30,8 @@
       catch {
         case exn: Throwable =>
           if (debug) exn.printStackTrace
-          System.err.println(Exn.message(exn))
-          2
+          System.err.println(Exn.error_message(exn))
+          Exn.return_code(exn, 2)
       }
     sys.exit(rc)
   }
diff -r 558afd429255 -r 140e6d01c481 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -58,7 +58,7 @@
         Exn.capture { f(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
-          case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
+          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
diff -r 558afd429255 -r 140e6d01c481 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -107,7 +107,7 @@
           if (rc != 0) error(output)
 
           val entries =
-            (for (entry <- File.read(dump) split "\0" if entry != "") yield {
+            (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
               val i = entry.indexOf('=')
               if (i <= 0) (entry -> "")
               else (entry.substring(0, i) -> entry.substring(i + 1))
@@ -332,7 +332,7 @@
         kill_cmd(signal)
         kill_cmd("0") == 0
       }
-      catch { case _: InterruptedException => true }
+      catch { case Exn.Interrupt() => true }
     }
 
     private def multi_kill(signal: String): Boolean =
@@ -341,7 +341,7 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          try { Thread.sleep(100) } catch { case _: InterruptedException => }
+          try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
           count -= 1
         }
         else running = false
@@ -446,6 +446,19 @@
     def set_rc(i: Int): Bash_Result = copy(rc = i)
   }
 
+  private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
+  {
+    private var count = 0L
+    def apply(progress: String => Unit)(line: String): Unit = synchronized {
+      progress(line)
+      count = count + line.length + 1
+      progress_limit match {
+        case Some(limit) if count > limit => proc.terminate
+        case _ =>
+      }
+    }
+  }
+
   def bash_env(cwd: JFile, env: Map[String, String], script: String,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
@@ -456,17 +469,7 @@
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
       proc.stdin.close
 
-      val limited = new Object {
-        private var count = 0L
-        def apply(progress: String => Unit)(line: String): Unit = synchronized {
-          progress(line)
-          count = count + line.length + 1
-          progress_limit match {
-            case Some(limit) if count > limit => proc.terminate
-            case _ =>
-          }
-        }
-      }
+      val limited = new Limited_Progress(proc, progress_limit)
       val (_, stdout) =
         Simple_Thread.future("bash_stdout") {
           File.read_lines(proc.stdout, limited(progress_stdout))
@@ -478,7 +481,7 @@
 
       val rc =
         try { proc.join }
-        catch { case e: InterruptedException => proc.terminate; 130 }
+        catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
       Bash_Result(stdout.join, stderr.join, rc)
     }
   }
diff -r 558afd429255 -r 140e6d01c481 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -423,6 +423,8 @@
       verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
+          if (progress.stopped) throw Exn.Interrupt()
+
           try {
             val (preloaded, parent_syntax) =
               info.parent match {
@@ -605,7 +607,7 @@
       args_file.delete
       timer.map(_.cancel())
 
-      if (res.rc == 130) {
+      if (res.rc == Exn.Interrupt.return_code) {
         if (timeout) res.add_err("*** Timeout").set_rc(1)
         else res.add_err("*** Interrupt")
       }
@@ -832,7 +834,7 @@
 
                 File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
                 progress.echo(name + " FAILED")
-                if (res.rc != 130) {
+                if (res.rc != Exn.Interrupt.return_code) {
                   progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
                   val lines = res.out_lines.filterNot(_.startsWith("\f"))
                   val tail = lines.drop(lines.length - 20 max 0)
diff -r 558afd429255 -r 140e6d01c481 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Tools/main.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,7 @@
     def exit_error(exn: Throwable): Nothing =
     {
       GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
-      system_dialog.return_code(2)
+      system_dialog.return_code(Exn.return_code(exn, 2))
       system_dialog.join_exit
     }
 
@@ -60,7 +60,9 @@
                     build_heap = true, more_dirs = more_dirs,
                     system_mode = system_mode, sessions = List(session)))
               }
-              catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+              catch {
+                case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
+              }
 
             system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
             system_dialog.return_code(rc)
@@ -155,7 +157,7 @@
       catch { case exn: Throwable => exit_error(exn) }
 
       if (system_dialog.stopped) {
-        system_dialog.return_code(130)
+        system_dialog.return_code(Exn.Interrupt.return_code)
         system_dialog.join_exit
       }
     }
@@ -195,7 +197,7 @@
           val path = (new JFile(isabelle_home, link)).toPath
 
           val writer = Files.newBufferedWriter(path, UTF8.charset)
-          try { writer.write("!<symlink>" + content + "\0") }
+          try { writer.write("!<symlink>" + content + "\u0000") }
           finally { writer.close }
 
           Files.setAttribute(path, "dos:system", true)
diff -r 558afd429255 -r 140e6d01c481 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/build-jars	Wed Apr 23 17:05:48 2014 +0200
@@ -232,13 +232,6 @@
   isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \
     fail "Failed to produce $TARGET"
 
-  cp "$SCALA_HOME/lib/scala-compiler.jar" \
-    "$SCALA_HOME/lib/scala-library.jar" \
-    "$SCALA_HOME/lib/scala-swing.jar" \
-    "$SCALA_HOME/lib/scala-actors.jar" \
-    "$SCALA_HOME/lib/scala-reflect.jar" \
-    "$TARGET_DIR"
-
   popd >/dev/null
 
   rm -rf classes
diff -r 558afd429255 -r 140e6d01c481 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/library.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -186,5 +186,5 @@
     new java.util.concurrent.Callable[A] { def call = f() }
 
   val default_thread_pool =
-    scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
+    scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
 }
diff -r 558afd429255 -r 140e6d01c481 src/Tools/Graphview/lib/Tools/graphview
--- a/src/Tools/Graphview/lib/Tools/graphview	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Wed Apr 23 17:05:48 2014 +0200
@@ -139,7 +139,7 @@
   rm -rf classes && mkdir classes
 
   (
-    #workaround for scalac 2.10.2
+    #FIXME workaround for scalac 2.11.0
     function stty() { :; }
     export -f stty
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -34,7 +34,7 @@
           case _ => error("Bad arguments:\n" + cat_lines(args))
         }
       }
-      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
+      catch { case exn: Throwable => println(Exn.error_message(exn)); sys.exit(1) }
 
     val top = new MainFrame {
       iconImage = GUI.isabelle_image()
diff -r 558afd429255 -r 140e6d01c481 src/Tools/Graphview/src/mutator_event.scala
--- a/src/Tools/Graphview/src/mutator_event.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -28,8 +28,8 @@
   {
     private val receivers = new mutable.ListBuffer[Receiver]
 
-    def += (r: Receiver) { Swing_Thread.require(); receivers += r }
-    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
-    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+    def += (r: Receiver) { Swing_Thread.require {}; receivers += r }
+    def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r }
+    def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) }
   }
 }
\ No newline at end of file
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Apr 23 17:05:48 2014 +0200
@@ -312,7 +312,7 @@
 
   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   (
-    #workaround for scalac 2.10.2
+    #FIXME workaround for scalac 2.11.0
     function stty() { :; }
     export -f stty
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -16,7 +16,7 @@
 {
   def action(view: View, text: String, elem: XML.Elem)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     Document_View(view.getTextArea) match {
       case Some(doc_view) =>
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -49,7 +49,7 @@
 
     def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       text_area.getClientProperty(key) match {
         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
         case _ => None
@@ -75,7 +75,7 @@
 
     def exit(text_area: JEditTextArea)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       apply(text_area) match {
         case None =>
         case Some(text_area_completion) =>
@@ -95,7 +95,7 @@
 
     def dismissed(text_area: TextArea): Boolean =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       apply(text_area) match {
         case Some(text_area_completion) => text_area_completion.dismissed()
         case None => false
@@ -194,7 +194,7 @@
 
     private def insert(item: Completion.Item)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val buffer = text_area.getBuffer
       val range = item.range
@@ -358,7 +358,7 @@
 
     def input(evt: KeyEvent)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       if (PIDE.options.bool("jedit_completion")) {
         if (!evt.isConsumed) {
@@ -391,7 +391,7 @@
 
     def dismissed(): Boolean =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       completion_popup match {
         case Some(completion) =>
@@ -460,7 +460,7 @@
 
     private def insert(item: Completion.Item)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val range = item.range
       if (text_field.isEditable && range.length > 0) {
@@ -574,7 +574,7 @@
 {
   completion =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   require(!items.isEmpty)
   val multi = items.length > 1
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,7 @@
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
       case _ => None
@@ -34,7 +34,7 @@
 
   def exit(buffer: Buffer)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(buffer) match {
       case None =>
       case Some(model) =>
@@ -46,7 +46,7 @@
 
   def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(buffer).map(_.deactivate)
     val model = new Document_Model(session, buffer, node_name)
     buffer.setProperty(key, model)
@@ -65,7 +65,7 @@
 
   def node_header(): Document.Node.Header =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
@@ -88,7 +88,7 @@
   def node_required: Boolean = _node_required
   def node_required_=(b: Boolean)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     if (_node_required != b && is_theory) {
       _node_required = b
       PIDE.options_changed()
@@ -101,7 +101,7 @@
 
   def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
 
   def apply(text_area: TextArea): Option[Document_View] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     text_area.getClientProperty(key) match {
       case doc_view: Document_View => Some(doc_view)
       case _ => None
@@ -38,7 +38,7 @@
 
   def exit(text_area: JEditTextArea)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(text_area) match {
       case None =>
       case Some(doc_view) =>
@@ -73,7 +73,7 @@
 
   def perspective(snapshot: Document.Snapshot): Text.Perspective =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val active_command =
     {
@@ -127,7 +127,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       rich_text_area.robust_body(()) {
-        Swing_Thread.assert()
+        Swing_Thread.assert {}
 
         val gutter = text_area.getGutter
         val width = GutterOptionPane.getSelectionAreaWidth
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -54,7 +54,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/font_info.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -42,7 +42,7 @@
   {
     private def change_size(change: Float => Float)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val size0 = main_size()
       val size = restrict_size(change(size0)).round
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
 
   private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     implicit_snapshot = snapshot
     implicit_graph = graph
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -30,7 +30,7 @@
 
   private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     implicit_snapshot = snapshot
     implicit_results = results
@@ -74,7 +74,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -153,7 +153,7 @@
 
   def continuous_checking_=(b: Boolean)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (continuous_checking != b) {
       PIDE.options.bool(CONTINUOUS_CHECKING) = b
@@ -179,7 +179,7 @@
 
   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     PIDE.document_model(view.getBuffer) match {
       case Some(model) =>
         model.node_required = (if (toggle) !model.node_required else set)
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
 
   def logic_selector(autosave: Boolean): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val entries =
       new Logic_Entry("", "default (" + jedit_logic() + ")") ::
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -24,7 +24,7 @@
 
   override def flush()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val doc_blobs = PIDE.document_blobs()
     val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
@@ -50,7 +50,7 @@
 
   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
@@ -64,7 +64,7 @@
 
   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val text_area = view.getTextArea
     val buffer = view.getBuffer
@@ -125,7 +125,7 @@
 
   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     push_position(view)
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
 
   def window_geometry(outer: Container, inner: Component): Window_Geometry =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val old_content = dummy_window.getContentPane
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -36,7 +36,7 @@
 
   def make_color_component(opt: Options.Opt): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
@@ -55,7 +55,7 @@
 
   def make_component(opt: Options.Opt): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -85,26 +85,26 @@
 
   /* file content */
 
-  def file_content(buffer: Buffer): Bytes =
+  private class File_Content_Output(buffer: Buffer) extends
+    ByteArrayOutputStream(buffer.getLength + 1)
+  {
+    def content(): Bytes = Bytes(this.buf, 0, this.count)
+  }
+
+  private class File_Content(buffer: Buffer) extends
+    BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
   {
-    val path = buffer.getPath
-    val vfs = VFSManager.getVFSForPath(path)
-    val content =
-      new BufferIORequest(null, buffer, null, vfs, path) {
-        def _run() { }
-        def apply(): Bytes =
-        {
-          val out =
-            new ByteArrayOutputStream(buffer.getLength + 1) {
-              def content(): Bytes = Bytes(this.buf, 0, this.count)
-            }
-          write(buffer, out)
-          out.content()
-        }
-      }
-    content()
+    def _run() { }
+    def content(): Bytes =
+    {
+      val out = new File_Content_Output(buffer)
+      write(buffer, out)
+      out.content()
+    }
   }
 
+  def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+
 
   /* theory text edits */
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -40,7 +40,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
@@ -48,7 +48,7 @@
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val (new_snapshot, new_command, new_results) =
       PIDE.editor.current_node_snapshot(view) match {
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -278,7 +278,7 @@
 
   override def handleMessage(message: EBMessage)
   {
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
       message match {
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -59,7 +59,7 @@
 {
   text_area =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   private var current_font_info: Font_Info = Font_Info.main()
   private var current_body: XML.Body = Nil
@@ -77,7 +77,7 @@
 
   def refresh()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val font = current_font_info.font
     getPainter.setFont(font)
@@ -142,7 +142,7 @@
 
   def resize(font_info: Font_Info)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     current_font_info = font_info
     refresh()
@@ -150,7 +150,7 @@
 
   def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     require(!base_snapshot.is_outdated)
 
     current_base_snapshot = base_snapshot
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -30,7 +30,7 @@
 
   private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (stack.contains(tip)) Some(stack.span(_ != tip))
     else None
@@ -47,7 +47,7 @@
     results: Command.Results,
     info: Text.Info[XML.Body])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     stack match {
       case top :: _ if top.results == results && top.info == info =>
@@ -173,7 +173,7 @@
 {
   tip =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
 
   /* controls */
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/process_indicator.scala
--- a/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,8 @@
     space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
       JEdit_Lib.load_image_icon(name).getImage)
 
-  private val animation = new ImageIcon(passive_icon) {
+  private class Animation extends ImageIcon(passive_icon)
+  {
     private var current_frame = 0
     private val timer =
       new Timer(0, new ActionListener {
@@ -52,6 +53,8 @@
       }
     }
   }
+
+  private val animation = new Animation
   label.icon = animation
 
   def component: Component = label
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -40,7 +40,7 @@
   def robust_body[A](default: A)(body: => A): A =
   {
     try {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       if (buffer == text_area.getBuffer) body
       else {
         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -21,7 +21,7 @@
 
 class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   /* component state -- owned by Swing thread */
 
@@ -61,7 +61,7 @@
 
   private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     val questions = context.questions.values
     if (do_auto_reply && !questions.isEmpty)
     {
@@ -147,7 +147,7 @@
 
   override def init()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     PIDE.session.global_options += main_actor
     PIDE.session.commands_changed += main_actor
@@ -158,7 +158,7 @@
 
   override def exit()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     PIDE.session.global_options -= main_actor
     PIDE.session.commands_changed -= main_actor
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -150,7 +150,7 @@
 class Simplifier_Trace_Window(
   view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
 {
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   val area = new Pretty_Text_Area(view)
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -55,7 +55,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -105,7 +105,7 @@
 
   def dictionaries_selector(): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -23,7 +23,7 @@
 
   private def update_syslog()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val text = PIDE.session.current_syslog()
     if (text != syslog.text) syslog.text = text
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -64,7 +64,7 @@
   override def paintComponent(gfx: Graphics)
   {
     super.paintComponent(gfx)
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     doc_view.rich_text_area.robust_body(()) {
       JEdit_Lib.buffer_lock(buffer) {
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
 
   private def handle_phase(phase: Session.Phase)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     session_phase.text = " " + phase_text(phase) + " "
   }
 
@@ -193,7 +193,7 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -152,7 +152,7 @@
 
   private def make_entries(): List[Entry] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val name =
       Document_View(view.getTextArea) match {
@@ -175,7 +175,7 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
 
diff -r 558afd429255 -r 140e6d01c481 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Apr 23 17:05:48 2014 +0200
@@ -42,7 +42,7 @@
 
   def edit_control_style(text_area: TextArea, control: String)
   {
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     val buffer = text_area.getBuffer