# HG changeset patch
# User wenzelm
# Date 1446555274 -3600
# Node ID 0d4ee4168e41694baabbe92dfe46e86298c6cbaa
# Parent  e27cfd2bf094019f82911b6f4fbd2f00af2c159d
clarified modules;

diff -r e27cfd2bf094 -r 0d4ee4168e41 Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/Admin/polyml/future/ROOT.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/bash_windows.ML
--- a/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/future.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -18,7 +18,7 @@
 object Future
 {
   lazy val execution_context: ExecutionContextExecutor =
-    ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
+    ExecutionContext.fromExecutorService(Standard_Thread.default_pool)
 
   def value[A](x: A): Future[A] = new Finished_Future(x)
 
diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -30,7 +30,7 @@
       try {
         state.change(_ =>
           (xs.iterator.zipWithIndex.map({ case (x, self) =>
-            Simple_Thread.submit_task {
+            Standard_Thread.submit_task {
               val result = Exn.capture { f(x) }
               result match { case Exn.Exn(_) => cancel_other(self) case _ => }
               result
diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Nov 03 11:24:42 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Tue Nov 03 11:24:42 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 => 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 e27cfd2bf094 -r 0d4ee4168e41 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 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 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 13:54:34 2015 +0100
@@ -0,0 +1,110 @@
+/*  Title:      Pure/Concurrent/standard_thread.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Standard thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
+  TimeUnit, LinkedBlockingQueue}
+
+
+object Standard_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 [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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/PIDE/prover.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -122,7 +122,7 @@
   /** process manager **/
 
   private val (_, process_result) =
-    Simple_Thread.future("process_result") { system_process.join }
+    Standard_Thread.future("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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/ROOT	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/ROOT.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/System/invoke_scala.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -94,7 +94,7 @@
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
-          Simple_Thread.submit_task {
+          Standard_Thread.submit_task {
             val (tag, result) = Invoke_Scala.method(name, msg.text)
             fulfill(prover, id, tag, result)
           })
diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -329,11 +329,11 @@
 
       val limited = new Limited_Progress(proc, progress_limit)
       val (_, stdout) =
-        Simple_Thread.future("bash_stdout") {
+        Standard_Thread.future("bash_stdout") {
           File.read_lines(proc.stdout, limited(progress_stdout))
         }
       val (_, stderr) =
-        Simple_Thread.future("bash_stderr") {
+        Standard_Thread.future("bash_stderr") {
           File.read_lines(proc.stderr, limited(progress_stderr))
         }
 
diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/System/message_channel.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -599,7 +599,7 @@
       }
 
     private val (thread, result) =
-      Simple_Thread.future("build") {
+      Standard_Thread.future("build") {
         Isabelle_System.bash_env(info.dir.file, env, script,
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Tools/debugger.ML	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Tools/debugger.scala	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/build-jars	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -130,7 +130,7 @@
 
       future_refresh.map(_.cancel(true))
       future_refresh =
-        Some(Simple_Thread.submit_task {
+        Some(Standard_Thread.submit_task {
           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 e27cfd2bf094 -r 0d4ee4168e41 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 13:54:34 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 e27cfd2bf094 -r 0d4ee4168e41 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 13:54:34 2015 +0100
@@ -128,7 +128,7 @@
             }
 
             future_refresh =
-              Some(Simple_Thread.submit_task {
+              Some(Standard_Thread.submit_task {
                 val line_count = overview.line_count
                 val char_count = overview.char_count
                 val L = overview.L