# HG changeset patch
# User wenzelm
# Date 1446570719 -3600
# Node ID 6d513469f9b220524859fed7427a0e44a8871076
# Parent  84901b8aa4f5ec408285d602590813ac6972efe9# Parent  91c3aedbfc5e2fd230f88237d2678f92e93f9f29
merged

diff -r 84901b8aa4f5 -r 6d513469f9b2 Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/Admin/polyml/future/ROOT.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -101,7 +101,7 @@
 use "General/properties.ML";
 use "General/timing.ML";
 
-use "Concurrent/simple_thread.ML";
+use "Concurrent/standard_thread.ML";
 use "Concurrent/synchronized.ML";
 use "General/markup.ML";
 use "Concurrent/single_assignment.ML";
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
+imports Cartesian_Euclidean_Space
 begin
 
 
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Complex Transcendental Functions\<close>
 
 theory Complex_Transcendental
-imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
+imports Complex_Analysis_Basics
 begin
 
 lemma cmod_add_real_less:
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -6,7 +6,7 @@
 section \<open>Multivariate calculus in Euclidean space\<close>
 
 theory Derivative
-imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
+imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
 begin
 
 lemma netlimit_at_vector: (* TODO: move *)
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -8,7 +8,10 @@
 section \<open>Limits on the Extended real number line\<close>
 
 theory Extended_Real_Limits
-  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
+imports
+  Topology_Euclidean_Space
+  "~~/src/HOL/Library/Extended_Real"
+  "~~/src/HOL/Library/Indicator_Function"
 begin
 
 lemma compact_UNIV:
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -1,12 +1,11 @@
-section \<open>polynomial functions: extremal behaviour and root counts\<close>
-
 (*  Author: John Harrison and Valentina Bruno
     Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
 *)
 
+section \<open>polynomial functions: extremal behaviour and root counts\<close>
+
 theory PolyRoots
 imports Complex_Main
-
 begin
 
 subsection\<open>Geometric progressions\<close>
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -1,8 +1,7 @@
-section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
+section \<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
 
 theory Weierstrass
 imports Uniform_Limit Path_Connected
-
 begin
 
 (*FIXME: simplification changes to be enforced globally*)
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Multivariate_Analysis/ex/Approximations.thy
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Tue Nov 03 18:11:59 2015 +0100
@@ -1,7 +1,7 @@
 section \<open>Binary Approximations to Constants\<close>
 
 theory Approximations
-imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
+imports Complex_Transcendental
 begin
 
 declare of_real_numeral [simp]
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -24,7 +24,7 @@
       Runtime.debugging NONE body () handle exn =>
         if Exn.is_interrupt exn then ()
         else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
-      Simple_Thread.attributes
+      Standard_Thread.attributes
         {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
 
 fun implode_message (workers, work) =
@@ -108,7 +108,7 @@
               NONE
             else
               let
-                val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
+                val _ = List.app (Standard_Thread.interrupt_unsynchronized o #1) canceling
                 val canceling' = filter (Thread.isActive o #1) canceling
                 val state' = make_state manager timeout_heap' active canceling' messages
               in SOME (map #2 timeout_threads, state') end
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -31,7 +31,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
@@ -83,7 +83,7 @@
           in () end;
 
     fun cleanup () =
-     (Simple_Thread.interrupt_unsynchronized system_thread;
+     (Standard_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
   in
     let
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/bash_windows.ML
--- a/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -35,7 +35,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
@@ -74,7 +74,7 @@
           in () end;
 
     fun cleanup () =
-     (Simple_Thread.interrupt_unsynchronized system_thread;
+     (Standard_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
   in
     let
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -32,7 +32,7 @@
   private var active = true
   private val mailbox = Mailbox[Option[Consumer_Thread.Request[A]]]
 
-  private val thread = Simple_Thread.fork(name, daemon) { main_loop(Nil) }
+  private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
   def is_active: Boolean = active && thread.isAlive
 
   private def failure(exn: Throwable): Unit =
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -105,7 +105,7 @@
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
   else
-    SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
+    SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
       manager_loop);
 
 fun shutdown () =
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -184,14 +184,14 @@
   let
     val running = Task_Queue.cancel (! queue) group;
     val _ = running |> List.app (fn thread =>
-      if Simple_Thread.is_self thread then ()
-      else Simple_Thread.interrupt_unsynchronized thread);
+      if Standard_Thread.is_self thread then ()
+      else Standard_Thread.interrupt_unsynchronized thread);
   in running end;
 
 fun cancel_all () = (*requires SYNCHRONIZED*)
   let
     val (groups, threads) = Task_Queue.cancel_all (! queue);
-    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+    val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
   in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -264,7 +264,7 @@
       Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
     val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
     val worker =
-      Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+      Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
         (fn () => worker_loop name);
   in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -367,7 +367,7 @@
   if scheduler_active () then ()
   else
     scheduler :=
-      SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+      SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
         scheduler_loop));
 
 
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/future.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -2,31 +2,24 @@
     Module:     PIDE
     Author:     Makarius
 
-Value-oriented parallel execution via futures and promises in Scala -- with
-signatures as in Isabelle/ML.
+Value-oriented parallel execution via futures and promises.
 */
 
 package isabelle
 
 
-import scala.util.{Success, Failure}
-import scala.concurrent.{ExecutionContext, ExecutionContextExecutor,
-  Future => Scala_Future, Promise => Scala_Promise, Await}
-import scala.concurrent.duration.Duration
+import java.util.concurrent.Callable
 
 
+/* futures and promises */
+
 object Future
 {
-  lazy val execution_context: ExecutionContextExecutor =
-    ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
-
-  def value[A](x: A): Future[A] = new Finished_Future(x)
-
-  def fork[A](body: => A): Future[A] =
-    new Pending_Future(Scala_Future[A](body)(execution_context))
-
-  def promise[A]: Promise[A] =
-    new Promise_Future[A](Scala_Promise[A]())
+  def value[A](x: A): Future[A] = new Value_Future(x)
+  def fork[A](body: => A): Future[A] = new Task_Future[A](body)
+  def promise[A]: Promise[A] = new Promise_Future[A]
+  def thread[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
+    new Thread_Future[A](name, daemon, body)
 }
 
 trait Future[A]
@@ -34,8 +27,10 @@
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
   def get_finished: A = { require(is_finished); Exn.release(peek.get) }
-  def join: A
+  def join_result: Exn.Result[A]
+  def join: A = Exn.release(join_result)
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }
+  def cancel: Unit
 
   override def toString: String =
     peek match {
@@ -47,46 +42,103 @@
 
 trait Promise[A] extends Future[A]
 {
-  def cancel: Unit
   def fulfill_result(res: Exn.Result[A]): Unit
   def fulfill(x: A): Unit
 }
 
 
-private class Finished_Future[A](x: A) extends Future[A]
+/* value future */
+
+private class Value_Future[A](x: A) extends Future[A]
 {
   val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
-  val join: A = x
+  def join_result: Exn.Result[A] = peek.get
+  def cancel {}
 }
 
-private class Pending_Future[A](future: Scala_Future[A]) extends Future[A]
+
+/* task future via thread pool */
+
+private class Task_Future[A](body: => A) extends Future[A]
 {
+  private sealed abstract class Status
+  private case object Ready extends Status
+  private case class Running(thread: Thread) extends Status
+  private case object Terminated extends Status
+  private case class Finished(result: Exn.Result[A]) extends Status
+
+  private val status = Synchronized[Status](Ready)
+
   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
+    status.value match {
+      case Finished(result) => Some(result)
+      case _ => None
+    }
+
+  private def try_run()
+  {
+    val do_run =
+      status.change_result {
+        case Ready => (true, Running(Thread.currentThread))
+        case st => (false, st)
+      }
+    if (do_run) {
+      val result = Exn.capture(body)
+      status.change(_ => Terminated)
+      status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
     }
-  override def is_finished: Boolean = future.isCompleted
+  }
+  private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body })
 
-  def join: A = Await.result(future, Duration.Inf)
-  override def map[B](f: A => B): Future[B] =
-    new Pending_Future[B](future.map(f)(Future.execution_context))
+  def join_result: Exn.Result[A] =
+  {
+    try_run()
+    status.guarded_access {
+      case st @ Finished(result) => Some((result, st))
+      case _ => None
+    }
+  }
+
+  def cancel =
+  {
+    status.change {
+      case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
+      case st @ Running(thread) => thread.interrupt; st
+      case st => st
+    }
+  }
 }
 
-private class Promise_Future[A](promise: Scala_Promise[A])
-  extends Pending_Future(promise.future) with Promise[A]
+
+/* promise future */
+
+private class Promise_Future[A] extends Promise[A]
 {
-  override def is_finished: Boolean = promise.isCompleted
+  private val state = Synchronized[Option[Exn.Result[A]]](None)
+  def peek: Option[Exn.Result[A]] = state.value
+
+  def join_result: Exn.Result[A] =
+    state.guarded_access(st => if (st.isEmpty) None else Some((st.get, st)))
+
+  def fulfill_result(result: Exn.Result[A]): Unit =
+    state.change(st => if (st.isEmpty) Some(result) else throw new IllegalStateException)
+
+  def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
 
   def cancel: Unit =
-    try { fulfill_result(Exn.Exn(Exn.Interrupt())) }
-    catch { case _: IllegalStateException => }
+    state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
+}
+
+
+/* thread future */
 
-  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 fulfill(x: A): Unit = promise.success(x)
+private class Thread_Future[A](name: String, daemon: Boolean, body: => A) extends Future[A]
+{
+  private val result = Future.promise[A]
+  private val thread =
+    Standard_Thread.fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+
+  def peek: Option[Exn.Result[A]] = result.peek
+  def join_result: Exn.Result[A] = result.join_result
+  def cancel: Unit = thread.interrupt
 }
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -8,38 +8,34 @@
 package isabelle
 
 
-import java.util.concurrent.{Future => JFuture, CancellationException}
-
-
 object Par_List
 {
   def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
     if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
     else {
-      val state = Synchronized((List.empty[JFuture[Exn.Result[B]]], false))
+      val state = Synchronized((List.empty[Future[B]], false))
 
       def cancel_other(self: Int = -1): Unit =
-        state.change { case (tasks, canceled) =>
+        state.change { case (futures, canceled) =>
           if (!canceled) {
-            for ((task, i) <- tasks.iterator.zipWithIndex if i != self)
-              task.cancel(true)
+            for ((future, i) <- futures.iterator.zipWithIndex if i != self)
+              future.cancel
           }
-          (tasks, true)
+          (futures, true)
         }
 
       try {
         state.change(_ =>
           (xs.iterator.zipWithIndex.map({ case (x, self) =>
-            Simple_Thread.submit_task {
-              val result = Exn.capture { f(x) }
-              result match { case Exn.Exn(_) => cancel_other(self) case _ => }
-              result
+            Future.fork {
+              Exn.capture { f(x) } match {
+                case Exn.Exn(exn) => cancel_other(self); throw exn
+                case Exn.Res(res) => res
+              }
             }
           }).toList, false))
 
-        state.value._1.map(future =>
-          try { future.get }
-          catch { case _: CancellationException => Exn.Exn(Exn.Interrupt()): Exn.Result[B] })
+        state.value._1.map(_.join_result)
       }
       finally { cancel_other() }
     }
@@ -65,4 +61,3 @@
   def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
   def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
 }
-
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Nov 03 15:24:24 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title:      Pure/Concurrent/simple_thread.ML
-    Author:     Makarius
-
-Simplified thread operations.
-*)
-
-signature SIMPLE_THREAD =
-sig
-  val is_self: Thread.thread -> bool
-  val get_name: unit -> string option
-  val the_name: unit -> string
-  type params = {name: string, stack_limit: int option, interrupts: bool}
-  val attributes: params -> Thread.threadAttribute list
-  val fork: params -> (unit -> unit) -> Thread.thread
-  val join: Thread.thread -> unit
-  val interrupt_unsynchronized: Thread.thread -> unit
-end;
-
-structure Simple_Thread: SIMPLE_THREAD =
-struct
-
-(* self *)
-
-fun is_self thread = Thread.equal (Thread.self (), thread);
-
-
-(* unique name *)
-
-local
-  val tag = Universal.tag () : string Universal.tag;
-  val count = Counter.make ();
-in
-
-fun get_name () = Thread.getLocal tag;
-
-fun the_name () =
-  (case get_name () of
-    NONE => raise Fail "Unknown thread name"
-  | SOME name => name);
-
-fun set_name base =
-  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
-
-end;
-
-
-(* fork *)
-
-type params = {name: string, stack_limit: int option, interrupts: bool};
-
-fun attributes ({stack_limit, interrupts, ...}: params) =
-  ML_Stack.limit stack_limit @
-  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
-
-fun fork (params: params) body =
-  Thread.fork (fn () =>
-    print_exception_trace General.exnMessage tracing (fn () =>
-      (set_name (#name params); body ())
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
-    attributes params);
-
-
-(* join *)
-
-fun join thread =
-  while Thread.isActive thread
-  do OS.Process.sleep (seconds 0.1);
-
-
-(* interrupt *)
-
-fun interrupt_unsynchronized thread =
-  Thread.interrupt thread handle Thread _ => ();
-
-end;
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Tue Nov 03 15:24:24 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-/*  Title:      Pure/Concurrent/simple_thread.scala
-    Module:     PIDE
-    Author:     Makarius
-
-Simplified thread operations.
-*/
-
-package isabelle
-
-
-import java.lang.Thread
-import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
-  TimeUnit, LinkedBlockingQueue}
-
-
-object Simple_Thread
-{
-  /* plain thread */
-
-  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
-  {
-    val thread =
-      if (name == null || name == "") new Thread() { override def run = body }
-      else new Thread(name) { override def run = body }
-    thread.setDaemon(daemon)
-    thread.start
-    thread
-  }
-
-
-  /* future result via thread */
-
-  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
-  {
-    val result = Future.promise[A]
-    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
-    (thread, result)
-  }
-
-
-  /* thread pool */
-
-  lazy val default_pool =
-    {
-      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
-      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
-    }
-
-  def submit_task[A](body: => A): JFuture[A] =
-    default_pool.submit(new Callable[A] { def call = body })
-
-
-  /* delayed events */
-
-  final class Delay private [Simple_Thread](
-    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
-  {
-    private var running: Option[Event_Timer.Request] = None
-
-    private def run: Unit =
-    {
-      val do_run = synchronized {
-        if (running.isDefined) { running = None; true } else false
-      }
-      if (do_run) event
-    }
-
-    def invoke(): Unit = synchronized
-    {
-      val new_run =
-        running match {
-          case Some(request) => if (first) false else { request.cancel; cancel(); true }
-          case None => true
-        }
-      if (new_run)
-        running = Some(Event_Timer.request(Time.now() + delay)(run))
-    }
-
-    def revoke(): Unit = synchronized
-    {
-      running match {
-        case Some(request) => request.cancel; cancel(); running = None
-        case None => cancel()
-      }
-    }
-
-    def postpone(alt_delay: Time): Unit = synchronized
-    {
-      running match {
-        case Some(request) =>
-          val alt_time = Time.now() + alt_delay
-          if (request.time < alt_time && request.cancel) {
-            cancel()
-            running = Some(Event_Timer.request(alt_time)(run))
-          }
-          else cancel()
-        case None => cancel()
-      }
-    }
-  }
-
-  // delayed event after first invocation
-  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
-    new Delay(true, delay, cancel, event)
-
-  // delayed event after last invocation
-  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
-    new Delay(false, delay, cancel, event)
-}
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/standard_thread.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/standard_thread.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -0,0 +1,75 @@
+(*  Title:      Pure/Concurrent/standard_thread.ML
+    Author:     Makarius
+
+Standard thread operations.
+*)
+
+signature STANDARD_THREAD =
+sig
+  val is_self: Thread.thread -> bool
+  val get_name: unit -> string option
+  val the_name: unit -> string
+  type params = {name: string, stack_limit: int option, interrupts: bool}
+  val attributes: params -> Thread.threadAttribute list
+  val fork: params -> (unit -> unit) -> Thread.thread
+  val join: Thread.thread -> unit
+  val interrupt_unsynchronized: Thread.thread -> unit
+end;
+
+structure Standard_Thread: STANDARD_THREAD =
+struct
+
+(* self *)
+
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
+
+(* unique name *)
+
+local
+  val tag = Universal.tag () : string Universal.tag;
+  val count = Counter.make ();
+in
+
+fun get_name () = Thread.getLocal tag;
+
+fun the_name () =
+  (case get_name () of
+    NONE => raise Fail "Unknown thread name"
+  | SOME name => name);
+
+fun set_name base =
+  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
+  ML_Stack.limit stack_limit @
+  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+
+fun fork (params: params) body =
+  Thread.fork (fn () =>
+    print_exception_trace General.exnMessage tracing (fn () =>
+      (set_name (#name params); body ())
+        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
+    attributes params);
+
+
+(* join *)
+
+fun join thread =
+  while Thread.isActive thread
+  do OS.Process.sleep (seconds 0.1);
+
+
+(* interrupt *)
+
+fun interrupt_unsynchronized thread =
+  Thread.interrupt thread handle Thread _ => ();
+
+end;
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/standard_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/standard_thread.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -0,0 +1,101 @@
+/*  Title:      Pure/Concurrent/standard_thread.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Standard thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue}
+
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor}
+
+
+object Standard_Thread
+{
+  /* fork */
+
+  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
+  {
+    val thread =
+      if (name == null || name == "") new Thread() { override def run = body }
+      else new Thread(name) { override def run = body }
+    thread.setDaemon(daemon)
+    thread.start
+    thread
+  }
+
+
+  /* pool */
+
+  lazy val pool: ThreadPoolExecutor =
+    {
+      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+    }
+
+  lazy val execution_context: ExecutionContextExecutor =
+    ExecutionContext.fromExecutorService(pool)
+
+
+  /* delayed events */
+
+  final class Delay private [Standard_Thread](
+    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
+  {
+    private var running: Option[Event_Timer.Request] = None
+
+    private def run: Unit =
+    {
+      val do_run = synchronized {
+        if (running.isDefined) { running = None; true } else false
+      }
+      if (do_run) event
+    }
+
+    def invoke(): Unit = synchronized
+    {
+      val new_run =
+        running match {
+          case Some(request) => if (first) false else { request.cancel; cancel(); true }
+          case None => cancel(); true
+        }
+      if (new_run)
+        running = Some(Event_Timer.request(Time.now() + delay)(run))
+    }
+
+    def revoke(): Unit = synchronized
+    {
+      running match {
+        case Some(request) => request.cancel; cancel(); running = None
+        case None => cancel()
+      }
+    }
+
+    def postpone(alt_delay: Time): Unit = synchronized
+    {
+      running match {
+        case Some(request) =>
+          val alt_time = Time.now() + alt_delay
+          if (request.time < alt_time && request.cancel) {
+            cancel()
+            running = Some(Event_Timer.request(alt_time)(run))
+          }
+          else cancel()
+        case None => cancel()
+      }
+    }
+  }
+
+  // delayed event after first invocation
+  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+    new Delay(true, delay, cancel, event)
+
+  // delayed event after last invocation
+  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+    new Delay(false, delay, cancel, event)
+}
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -22,7 +22,7 @@
 
       val request =
         Event_Timer.request (Time.+ (Time.now (), timeout))
-          (fn () => Simple_Thread.interrupt_unsynchronized self);
+          (fn () => Standard_Thread.interrupt_unsynchronized self);
 
       val result =
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -50,8 +50,8 @@
   /* delayed events */
 
   def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
+    : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
 
   def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
+    : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
 }
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/General/exn.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -58,7 +58,7 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
-    def expose() { if (Thread.interrupted()) throw apply() }
+    def expose() { if (Thread.interrupted) throw apply() }
     def impose() { Thread.currentThread.interrupt }
 
     def postpone[A](body: => A): Option[A] =
@@ -104,4 +104,3 @@
   def message(exn: Throwable): String =
     user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
 }
-
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/PIDE/prover.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -121,8 +121,8 @@
 
   /** process manager **/
 
-  private val (_, process_result) =
-    Simple_Thread.future("process_result") { system_process.join }
+  private val process_result =
+    Future.thread("process_result") { system_process.join }
 
   private def terminate_process()
   {
@@ -132,7 +132,7 @@
     }
   }
 
-  private val process_manager = Simple_Thread.fork("process_manager")
+  private val process_manager = Standard_Thread.fork("process_manager")
   {
     val (startup_failed, startup_errors) =
     {
@@ -230,7 +230,7 @@
       if (err) ("standard_error", system_process.stderr, Markup.STDERR)
       else ("standard_output", system_process.stdout, Markup.STDOUT)
 
-    Simple_Thread.fork(name) {
+    Standard_Thread.fork(name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
@@ -268,7 +268,7 @@
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
-    Simple_Thread.fork(name) {
+    Standard_Thread.fork(name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -291,7 +291,7 @@
       nodes = Set.empty
       commands = Set.empty
     }
-    private val delay_flush = Simple_Thread.delay_first(output_delay) { flush() }
+    private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
 
     def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
       assignment |= assign
@@ -353,7 +353,7 @@
 
   /* manager thread */
 
-  private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+  private val delay_prune = Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/ROOT	Tue Nov 03 18:11:59 2015 +0100
@@ -86,9 +86,9 @@
     "Concurrent/par_list.ML"
     "Concurrent/par_list_sequential.ML"
     "Concurrent/random.ML"
-    "Concurrent/simple_thread.ML"
     "Concurrent/single_assignment.ML"
     "Concurrent/single_assignment_sequential.ML"
+    "Concurrent/standard_thread.ML"
     "Concurrent/synchronized.ML"
     "Concurrent/synchronized_sequential.ML"
     "Concurrent/task_queue.ML"
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/ROOT.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -109,7 +109,7 @@
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
-use "Concurrent/simple_thread.ML";
+use "Concurrent/standard_thread.ML";
 
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/invoke_scala.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -8,7 +8,6 @@
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.util.concurrent.{Future => JFuture}
 
 import scala.util.matching.Regex
 
@@ -72,7 +71,7 @@
 
 class Invoke_Scala extends Session.Protocol_Handler
 {
-  private var futures = Map.empty[String, JFuture[Unit]]
+  private var futures = Map.empty[String, Future[Unit]]
 
   private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
@@ -83,9 +82,9 @@
       }
     }
 
-  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
+  private def cancel(prover: Prover, id: String, future: Future[Unit])
   {
-    future.cancel(true)
+    future.cancel
     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
   }
 
@@ -94,7 +93,7 @@
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
-          Simple_Thread.submit_task {
+          Future.fork {
             val (tag, result) = Invoke_Scala.method(name, msg.text)
             fulfill(prover, id, tag, result)
           })
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -328,14 +328,10 @@
       proc.stdin.close
 
       val limited = new Limited_Progress(proc, progress_limit)
-      val (_, stdout) =
-        Simple_Thread.future("bash_stdout") {
-          File.read_lines(proc.stdout, limited(progress_stdout))
-        }
-      val (_, stderr) =
-        Simple_Thread.future("bash_stderr") {
-          File.read_lines(proc.stderr, limited(progress_stderr))
-        }
+      val stdout =
+        Future.thread("bash_stdout") { File.read_lines(proc.stdout, limited(progress_stdout)) }
+      val stderr =
+        Future.thread("bash_stderr") { File.read_lines(proc.stderr, limited(progress_stderr)) }
 
       val rc =
         try { proc.join }
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/message_channel.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -60,11 +60,11 @@
     let
       val mbox = Mailbox.create ();
       val thread =
-        Simple_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+        Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
           (message_output mbox channel);
       fun send msg = Mailbox.send mbox (SOME msg);
       fun shutdown () =
-        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
+        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
     in Message_Channel {send = send, shutdown = shutdown} end
   else
     let
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -598,8 +598,8 @@
         """
       }
 
-    private val (thread, result) =
-      Simple_Thread.future("build") {
+    private val result =
+      Future.thread("build") {
         Isabelle_System.bash_env(info.dir.file, env, script,
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
@@ -614,7 +614,7 @@
           strict = false)
       }
 
-    def terminate: Unit = thread.interrupt
+    def terminate: Unit = result.cancel
     def is_finished: Boolean = result.is_finished
 
     @volatile private var was_timeout = false
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/debugger.ML	Tue Nov 03 18:11:59 2015 +0100
@@ -24,7 +24,7 @@
   if msg = "" then ()
   else
     Output.protocol_message
-      (Markup.debugger_output (Simple_Thread.the_name ()))
+      (Markup.debugger_output (Standard_Thread.the_name ()))
       [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
 
 val writeln_message = output_message Markup.writelnN;
@@ -255,7 +255,7 @@
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
-            (case Simple_Thread.get_name () of
+            (case Standard_Thread.get_name () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/debugger.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -114,7 +114,7 @@
   case object Update
 
   private val delay_update =
-    Simple_Thread.delay_first(global_state.value.session.output_delay) {
+    Standard_Thread.delay_first(global_state.value.session.output_delay) {
       global_state.value.session.debugger_updates.post(Update)
     }
 
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/build-jars	Tue Nov 03 18:11:59 2015 +0100
@@ -16,7 +16,7 @@
   Concurrent/future.scala
   Concurrent/mailbox.scala
   Concurrent/par_list.scala
-  Concurrent/simple_thread.scala
+  Concurrent/standard_thread.scala
   Concurrent/synchronized.scala
   GUI/color_value.scala
   GUI/gui.scala
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/active.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -30,7 +30,7 @@
             // FIXME avoid hard-wired stuff
             elem match {
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                Future.fork {
+                Standard_Thread.fork("browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
                   Isabelle_System.bash_env(null,
@@ -39,7 +39,7 @@
                 }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                Future.fork {
+                Standard_Thread.fork("graphview") {
                   val graph =
                     Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -59,7 +59,7 @@
         if (path.is_file)
           PIDE.editor.goto_file(true, view, File.platform_path(path))
         else {
-          Future.fork {
+          Standard_Thread.fork("documentation") {
             try { Doc.view(path) }
             catch {
               case exn: Throwable =>
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -194,7 +194,7 @@
     new Hyperlink {
       val external = true
       def follow(view: View): Unit =
-        Future.fork {
+        Standard_Thread.fork("hyperlink_url") {
           try { Isabelle_System.open(name) }
           catch {
             case exn: Throwable =>
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -10,7 +10,6 @@
 
 import isabelle._
 
-import java.util.concurrent.{Future => JFuture}
 import java.awt.{Color, Font, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
@@ -75,7 +74,7 @@
   private var current_base_results = Command.Results.empty
   private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
-  private var future_refresh: Option[JFuture[Unit]] = None
+  private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -128,9 +127,9 @@
       val base_results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin, metric)
 
-      future_refresh.map(_.cancel(true))
+      future_refresh.map(_.cancel)
       future_refresh =
-        Some(Simple_Thread.submit_task {
+        Some(Future.fork {
           val (text, rendering) =
             try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -165,7 +165,7 @@
           }
           finally {
             running.change(_ => None)
-            Thread.interrupted()
+            Thread.interrupted
           }
           GUI_Thread.later {
             if (err != null) err.commandDone()
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -161,7 +161,7 @@
     setLocationRelativeTo(view)
     setVisible(true)
 
-    Simple_Thread.fork("session_build") {
+    Standard_Thread.fork("session_build") {
       progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
 
       val (out, rc) =
diff -r 84901b8aa4f5 -r 6d513469f9b2 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 18:11:59 2015 +0100
@@ -11,7 +11,6 @@
 
 import scala.annotation.tailrec
 
-import java.util.concurrent.{Future => JFuture}
 import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
 import java.awt.event.{MouseAdapter, MouseEvent}
 import javax.swing.{JPanel, ToolTipManager}
@@ -102,8 +101,8 @@
 
   /* asynchronous refresh */
 
-  private var future_refresh: Option[JFuture[Unit]] = None
-  private def cancel(): Unit = future_refresh.map(_.cancel(true))
+  private var future_refresh: Option[Future[Unit]] = None
+  private def cancel(): Unit = future_refresh.map(_.cancel)
 
   def invoke(): Unit = delay_refresh.invoke()
   def revoke(): Unit = delay_refresh.revoke()
@@ -128,7 +127,7 @@
             }
 
             future_refresh =
-              Some(Simple_Thread.submit_task {
+              Some(Future.fork {
                 val line_count = overview.line_count
                 val char_count = overview.char_count
                 val L = overview.L