clarified modules;
authorwenzelm
Tue Nov 03 13:54:34 2015 +0100 (2015-11-03)
changeset 615560d4ee4168e41
parent 61555 e27cfd2bf094
child 61557 f6387515f951
clarified modules;
Admin/polyml/future/ROOT.ML
src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash_windows.ML
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/par_list.scala
src/Pure/Concurrent/simple_thread.ML
src/Pure/Concurrent/simple_thread.scala
src/Pure/Concurrent/standard_thread.ML
src/Pure/Concurrent/standard_thread.scala
src/Pure/Concurrent/time_limit.ML
src/Pure/GUI/gui_thread.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/session.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/message_channel.ML
src/Pure/Tools/build.scala
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
src/Pure/build-jars
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/session_build.scala
src/Tools/jEdit/src/text_overview.scala
     1.1 --- a/Admin/polyml/future/ROOT.ML	Tue Nov 03 11:24:42 2015 +0100
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Tue Nov 03 13:54:34 2015 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4  use "General/properties.ML";
     1.5  use "General/timing.ML";
     1.6  
     1.7 -use "Concurrent/simple_thread.ML";
     1.8 +use "Concurrent/standard_thread.ML";
     1.9  use "Concurrent/synchronized.ML";
    1.10  use "General/markup.ML";
    1.11  use "Concurrent/single_assignment.ML";
     2.1 --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 11:24:42 2015 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Nov 03 13:54:34 2015 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4        Runtime.debugging NONE body () handle exn =>
     2.5          if Exn.is_interrupt exn then ()
     2.6          else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
     2.7 -      Simple_Thread.attributes
     2.8 +      Standard_Thread.attributes
     2.9          {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
    2.10  
    2.11  fun implode_message (workers, work) =
    2.12 @@ -108,7 +108,7 @@
    2.13                NONE
    2.14              else
    2.15                let
    2.16 -                val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
    2.17 +                val _ = List.app (Standard_Thread.interrupt_unsynchronized o #1) canceling
    2.18                  val canceling' = filter (Thread.isActive o #1) canceling
    2.19                  val state' = make_state manager timeout_heap' active canceling' messages
    2.20                in SOME (map #2 timeout_threads, state') end
     3.1 --- a/src/Pure/Concurrent/bash.ML	Tue Nov 03 11:24:42 2015 +0100
     3.2 +++ b/src/Pure/Concurrent/bash.ML	Tue Nov 03 13:54:34 2015 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4      val _ = cleanup_files ();
     3.5  
     3.6      val system_thread =
     3.7 -      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
     3.8 +      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
     3.9          Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    3.10            let
    3.11              val _ = File.write script_path script;
    3.12 @@ -83,7 +83,7 @@
    3.13            in () end;
    3.14  
    3.15      fun cleanup () =
    3.16 -     (Simple_Thread.interrupt_unsynchronized system_thread;
    3.17 +     (Standard_Thread.interrupt_unsynchronized system_thread;
    3.18        cleanup_files ());
    3.19    in
    3.20      let
     4.1 --- a/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 11:24:42 2015 +0100
     4.2 +++ b/src/Pure/Concurrent/bash_windows.ML	Tue Nov 03 13:54:34 2015 +0100
     4.3 @@ -35,7 +35,7 @@
     4.4      val _ = cleanup_files ();
     4.5  
     4.6      val system_thread =
     4.7 -      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
     4.8 +      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
     4.9          Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    4.10            let
    4.11              val _ = File.write script_path script;
    4.12 @@ -74,7 +74,7 @@
    4.13            in () end;
    4.14  
    4.15      fun cleanup () =
    4.16 -     (Simple_Thread.interrupt_unsynchronized system_thread;
    4.17 +     (Standard_Thread.interrupt_unsynchronized system_thread;
    4.18        cleanup_files ());
    4.19    in
    4.20      let
     5.1 --- a/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 11:24:42 2015 +0100
     5.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Nov 03 13:54:34 2015 +0100
     5.3 @@ -32,7 +32,7 @@
     5.4    private var active = true
     5.5    private val mailbox = Mailbox[Option[Consumer_Thread.Request[A]]]
     5.6  
     5.7 -  private val thread = Simple_Thread.fork(name, daemon) { main_loop(Nil) }
     5.8 +  private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
     5.9    def is_active: Boolean = active && thread.isAlive
    5.10  
    5.11    private def failure(exn: Throwable): Unit =
     6.1 --- a/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 11:24:42 2015 +0100
     6.2 +++ b/src/Pure/Concurrent/event_timer.ML	Tue Nov 03 13:54:34 2015 +0100
     6.3 @@ -105,7 +105,7 @@
     6.4  fun manager_check manager =
     6.5    if is_some manager andalso Thread.isActive (the manager) then manager
     6.6    else
     6.7 -    SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
     6.8 +    SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
     6.9        manager_loop);
    6.10  
    6.11  fun shutdown () =
     7.1 --- a/src/Pure/Concurrent/future.ML	Tue Nov 03 11:24:42 2015 +0100
     7.2 +++ b/src/Pure/Concurrent/future.ML	Tue Nov 03 13:54:34 2015 +0100
     7.3 @@ -184,14 +184,14 @@
     7.4    let
     7.5      val running = Task_Queue.cancel (! queue) group;
     7.6      val _ = running |> List.app (fn thread =>
     7.7 -      if Simple_Thread.is_self thread then ()
     7.8 -      else Simple_Thread.interrupt_unsynchronized thread);
     7.9 +      if Standard_Thread.is_self thread then ()
    7.10 +      else Standard_Thread.interrupt_unsynchronized thread);
    7.11    in running end;
    7.12  
    7.13  fun cancel_all () = (*requires SYNCHRONIZED*)
    7.14    let
    7.15      val (groups, threads) = Task_Queue.cancel_all (! queue);
    7.16 -    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    7.17 +    val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
    7.18    in groups end;
    7.19  
    7.20  fun cancel_later group = (*requires SYNCHRONIZED*)
    7.21 @@ -264,7 +264,7 @@
    7.22        Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
    7.23      val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
    7.24      val worker =
    7.25 -      Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
    7.26 +      Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
    7.27          (fn () => worker_loop name);
    7.28    in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
    7.29    handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
    7.30 @@ -367,7 +367,7 @@
    7.31    if scheduler_active () then ()
    7.32    else
    7.33      scheduler :=
    7.34 -      SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
    7.35 +      SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
    7.36          scheduler_loop));
    7.37  
    7.38  
     8.1 --- a/src/Pure/Concurrent/future.scala	Tue Nov 03 11:24:42 2015 +0100
     8.2 +++ b/src/Pure/Concurrent/future.scala	Tue Nov 03 13:54:34 2015 +0100
     8.3 @@ -18,7 +18,7 @@
     8.4  object Future
     8.5  {
     8.6    lazy val execution_context: ExecutionContextExecutor =
     8.7 -    ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
     8.8 +    ExecutionContext.fromExecutorService(Standard_Thread.default_pool)
     8.9  
    8.10    def value[A](x: A): Future[A] = new Finished_Future(x)
    8.11  
     9.1 --- a/src/Pure/Concurrent/par_list.scala	Tue Nov 03 11:24:42 2015 +0100
     9.2 +++ b/src/Pure/Concurrent/par_list.scala	Tue Nov 03 13:54:34 2015 +0100
     9.3 @@ -30,7 +30,7 @@
     9.4        try {
     9.5          state.change(_ =>
     9.6            (xs.iterator.zipWithIndex.map({ case (x, self) =>
     9.7 -            Simple_Thread.submit_task {
     9.8 +            Standard_Thread.submit_task {
     9.9                val result = Exn.capture { f(x) }
    9.10                result match { case Exn.Exn(_) => cancel_other(self) case _ => }
    9.11                result
    10.1 --- a/src/Pure/Concurrent/simple_thread.ML	Tue Nov 03 11:24:42 2015 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,75 +0,0 @@
    10.4 -(*  Title:      Pure/Concurrent/simple_thread.ML
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Simplified thread operations.
    10.8 -*)
    10.9 -
   10.10 -signature SIMPLE_THREAD =
   10.11 -sig
   10.12 -  val is_self: Thread.thread -> bool
   10.13 -  val get_name: unit -> string option
   10.14 -  val the_name: unit -> string
   10.15 -  type params = {name: string, stack_limit: int option, interrupts: bool}
   10.16 -  val attributes: params -> Thread.threadAttribute list
   10.17 -  val fork: params -> (unit -> unit) -> Thread.thread
   10.18 -  val join: Thread.thread -> unit
   10.19 -  val interrupt_unsynchronized: Thread.thread -> unit
   10.20 -end;
   10.21 -
   10.22 -structure Simple_Thread: SIMPLE_THREAD =
   10.23 -struct
   10.24 -
   10.25 -(* self *)
   10.26 -
   10.27 -fun is_self thread = Thread.equal (Thread.self (), thread);
   10.28 -
   10.29 -
   10.30 -(* unique name *)
   10.31 -
   10.32 -local
   10.33 -  val tag = Universal.tag () : string Universal.tag;
   10.34 -  val count = Counter.make ();
   10.35 -in
   10.36 -
   10.37 -fun get_name () = Thread.getLocal tag;
   10.38 -
   10.39 -fun the_name () =
   10.40 -  (case get_name () of
   10.41 -    NONE => raise Fail "Unknown thread name"
   10.42 -  | SOME name => name);
   10.43 -
   10.44 -fun set_name base =
   10.45 -  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
   10.46 -
   10.47 -end;
   10.48 -
   10.49 -
   10.50 -(* fork *)
   10.51 -
   10.52 -type params = {name: string, stack_limit: int option, interrupts: bool};
   10.53 -
   10.54 -fun attributes ({stack_limit, interrupts, ...}: params) =
   10.55 -  ML_Stack.limit stack_limit @
   10.56 -  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
   10.57 -
   10.58 -fun fork (params: params) body =
   10.59 -  Thread.fork (fn () =>
   10.60 -    print_exception_trace General.exnMessage tracing (fn () =>
   10.61 -      (set_name (#name params); body ())
   10.62 -        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
   10.63 -    attributes params);
   10.64 -
   10.65 -
   10.66 -(* join *)
   10.67 -
   10.68 -fun join thread =
   10.69 -  while Thread.isActive thread
   10.70 -  do OS.Process.sleep (seconds 0.1);
   10.71 -
   10.72 -
   10.73 -(* interrupt *)
   10.74 -
   10.75 -fun interrupt_unsynchronized thread =
   10.76 -  Thread.interrupt thread handle Thread _ => ();
   10.77 -
   10.78 -end;
    11.1 --- a/src/Pure/Concurrent/simple_thread.scala	Tue Nov 03 11:24:42 2015 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,110 +0,0 @@
    11.4 -/*  Title:      Pure/Concurrent/simple_thread.scala
    11.5 -    Module:     PIDE
    11.6 -    Author:     Makarius
    11.7 -
    11.8 -Simplified thread operations.
    11.9 -*/
   11.10 -
   11.11 -package isabelle
   11.12 -
   11.13 -
   11.14 -import java.lang.Thread
   11.15 -import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
   11.16 -  TimeUnit, LinkedBlockingQueue}
   11.17 -
   11.18 -
   11.19 -object Simple_Thread
   11.20 -{
   11.21 -  /* plain thread */
   11.22 -
   11.23 -  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
   11.24 -  {
   11.25 -    val thread =
   11.26 -      if (name == null || name == "") new Thread() { override def run = body }
   11.27 -      else new Thread(name) { override def run = body }
   11.28 -    thread.setDaemon(daemon)
   11.29 -    thread.start
   11.30 -    thread
   11.31 -  }
   11.32 -
   11.33 -
   11.34 -  /* future result via thread */
   11.35 -
   11.36 -  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
   11.37 -  {
   11.38 -    val result = Future.promise[A]
   11.39 -    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
   11.40 -    (thread, result)
   11.41 -  }
   11.42 -
   11.43 -
   11.44 -  /* thread pool */
   11.45 -
   11.46 -  lazy val default_pool =
   11.47 -    {
   11.48 -      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
   11.49 -      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
   11.50 -      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
   11.51 -    }
   11.52 -
   11.53 -  def submit_task[A](body: => A): JFuture[A] =
   11.54 -    default_pool.submit(new Callable[A] { def call = body })
   11.55 -
   11.56 -
   11.57 -  /* delayed events */
   11.58 -
   11.59 -  final class Delay private [Simple_Thread](
   11.60 -    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
   11.61 -  {
   11.62 -    private var running: Option[Event_Timer.Request] = None
   11.63 -
   11.64 -    private def run: Unit =
   11.65 -    {
   11.66 -      val do_run = synchronized {
   11.67 -        if (running.isDefined) { running = None; true } else false
   11.68 -      }
   11.69 -      if (do_run) event
   11.70 -    }
   11.71 -
   11.72 -    def invoke(): Unit = synchronized
   11.73 -    {
   11.74 -      val new_run =
   11.75 -        running match {
   11.76 -          case Some(request) => if (first) false else { request.cancel; cancel(); true }
   11.77 -          case None => cancel(); true
   11.78 -        }
   11.79 -      if (new_run)
   11.80 -        running = Some(Event_Timer.request(Time.now() + delay)(run))
   11.81 -    }
   11.82 -
   11.83 -    def revoke(): Unit = synchronized
   11.84 -    {
   11.85 -      running match {
   11.86 -        case Some(request) => request.cancel; cancel(); running = None
   11.87 -        case None => cancel()
   11.88 -      }
   11.89 -    }
   11.90 -
   11.91 -    def postpone(alt_delay: Time): Unit = synchronized
   11.92 -    {
   11.93 -      running match {
   11.94 -        case Some(request) =>
   11.95 -          val alt_time = Time.now() + alt_delay
   11.96 -          if (request.time < alt_time && request.cancel) {
   11.97 -            cancel()
   11.98 -            running = Some(Event_Timer.request(alt_time)(run))
   11.99 -          }
  11.100 -          else cancel()
  11.101 -        case None => cancel()
  11.102 -      }
  11.103 -    }
  11.104 -  }
  11.105 -
  11.106 -  // delayed event after first invocation
  11.107 -  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
  11.108 -    new Delay(true, delay, cancel, event)
  11.109 -
  11.110 -  // delayed event after last invocation
  11.111 -  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
  11.112 -    new Delay(false, delay, cancel, event)
  11.113 -}
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Tue Nov 03 13:54:34 2015 +0100
    12.3 @@ -0,0 +1,75 @@
    12.4 +(*  Title:      Pure/Concurrent/standard_thread.ML
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Standard thread operations.
    12.8 +*)
    12.9 +
   12.10 +signature STANDARD_THREAD =
   12.11 +sig
   12.12 +  val is_self: Thread.thread -> bool
   12.13 +  val get_name: unit -> string option
   12.14 +  val the_name: unit -> string
   12.15 +  type params = {name: string, stack_limit: int option, interrupts: bool}
   12.16 +  val attributes: params -> Thread.threadAttribute list
   12.17 +  val fork: params -> (unit -> unit) -> Thread.thread
   12.18 +  val join: Thread.thread -> unit
   12.19 +  val interrupt_unsynchronized: Thread.thread -> unit
   12.20 +end;
   12.21 +
   12.22 +structure Standard_Thread: STANDARD_THREAD =
   12.23 +struct
   12.24 +
   12.25 +(* self *)
   12.26 +
   12.27 +fun is_self thread = Thread.equal (Thread.self (), thread);
   12.28 +
   12.29 +
   12.30 +(* unique name *)
   12.31 +
   12.32 +local
   12.33 +  val tag = Universal.tag () : string Universal.tag;
   12.34 +  val count = Counter.make ();
   12.35 +in
   12.36 +
   12.37 +fun get_name () = Thread.getLocal tag;
   12.38 +
   12.39 +fun the_name () =
   12.40 +  (case get_name () of
   12.41 +    NONE => raise Fail "Unknown thread name"
   12.42 +  | SOME name => name);
   12.43 +
   12.44 +fun set_name base =
   12.45 +  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
   12.46 +
   12.47 +end;
   12.48 +
   12.49 +
   12.50 +(* fork *)
   12.51 +
   12.52 +type params = {name: string, stack_limit: int option, interrupts: bool};
   12.53 +
   12.54 +fun attributes ({stack_limit, interrupts, ...}: params) =
   12.55 +  ML_Stack.limit stack_limit @
   12.56 +  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
   12.57 +
   12.58 +fun fork (params: params) body =
   12.59 +  Thread.fork (fn () =>
   12.60 +    print_exception_trace General.exnMessage tracing (fn () =>
   12.61 +      (set_name (#name params); body ())
   12.62 +        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
   12.63 +    attributes params);
   12.64 +
   12.65 +
   12.66 +(* join *)
   12.67 +
   12.68 +fun join thread =
   12.69 +  while Thread.isActive thread
   12.70 +  do OS.Process.sleep (seconds 0.1);
   12.71 +
   12.72 +
   12.73 +(* interrupt *)
   12.74 +
   12.75 +fun interrupt_unsynchronized thread =
   12.76 +  Thread.interrupt thread handle Thread _ => ();
   12.77 +
   12.78 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Pure/Concurrent/standard_thread.scala	Tue Nov 03 13:54:34 2015 +0100
    13.3 @@ -0,0 +1,110 @@
    13.4 +/*  Title:      Pure/Concurrent/standard_thread.scala
    13.5 +    Module:     PIDE
    13.6 +    Author:     Makarius
    13.7 +
    13.8 +Standard thread operations.
    13.9 +*/
   13.10 +
   13.11 +package isabelle
   13.12 +
   13.13 +
   13.14 +import java.lang.Thread
   13.15 +import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
   13.16 +  TimeUnit, LinkedBlockingQueue}
   13.17 +
   13.18 +
   13.19 +object Standard_Thread
   13.20 +{
   13.21 +  /* plain thread */
   13.22 +
   13.23 +  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
   13.24 +  {
   13.25 +    val thread =
   13.26 +      if (name == null || name == "") new Thread() { override def run = body }
   13.27 +      else new Thread(name) { override def run = body }
   13.28 +    thread.setDaemon(daemon)
   13.29 +    thread.start
   13.30 +    thread
   13.31 +  }
   13.32 +
   13.33 +
   13.34 +  /* future result via thread */
   13.35 +
   13.36 +  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
   13.37 +  {
   13.38 +    val result = Future.promise[A]
   13.39 +    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
   13.40 +    (thread, result)
   13.41 +  }
   13.42 +
   13.43 +
   13.44 +  /* thread pool */
   13.45 +
   13.46 +  lazy val default_pool =
   13.47 +    {
   13.48 +      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
   13.49 +      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
   13.50 +      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
   13.51 +    }
   13.52 +
   13.53 +  def submit_task[A](body: => A): JFuture[A] =
   13.54 +    default_pool.submit(new Callable[A] { def call = body })
   13.55 +
   13.56 +
   13.57 +  /* delayed events */
   13.58 +
   13.59 +  final class Delay private [Standard_Thread](
   13.60 +    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
   13.61 +  {
   13.62 +    private var running: Option[Event_Timer.Request] = None
   13.63 +
   13.64 +    private def run: Unit =
   13.65 +    {
   13.66 +      val do_run = synchronized {
   13.67 +        if (running.isDefined) { running = None; true } else false
   13.68 +      }
   13.69 +      if (do_run) event
   13.70 +    }
   13.71 +
   13.72 +    def invoke(): Unit = synchronized
   13.73 +    {
   13.74 +      val new_run =
   13.75 +        running match {
   13.76 +          case Some(request) => if (first) false else { request.cancel; cancel(); true }
   13.77 +          case None => cancel(); true
   13.78 +        }
   13.79 +      if (new_run)
   13.80 +        running = Some(Event_Timer.request(Time.now() + delay)(run))
   13.81 +    }
   13.82 +
   13.83 +    def revoke(): Unit = synchronized
   13.84 +    {
   13.85 +      running match {
   13.86 +        case Some(request) => request.cancel; cancel(); running = None
   13.87 +        case None => cancel()
   13.88 +      }
   13.89 +    }
   13.90 +
   13.91 +    def postpone(alt_delay: Time): Unit = synchronized
   13.92 +    {
   13.93 +      running match {
   13.94 +        case Some(request) =>
   13.95 +          val alt_time = Time.now() + alt_delay
   13.96 +          if (request.time < alt_time && request.cancel) {
   13.97 +            cancel()
   13.98 +            running = Some(Event_Timer.request(alt_time)(run))
   13.99 +          }
  13.100 +          else cancel()
  13.101 +        case None => cancel()
  13.102 +      }
  13.103 +    }
  13.104 +  }
  13.105 +
  13.106 +  // delayed event after first invocation
  13.107 +  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
  13.108 +    new Delay(true, delay, cancel, event)
  13.109 +
  13.110 +  // delayed event after last invocation
  13.111 +  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
  13.112 +    new Delay(false, delay, cancel, event)
  13.113 +}
    14.1 --- a/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 11:24:42 2015 +0100
    14.2 +++ b/src/Pure/Concurrent/time_limit.ML	Tue Nov 03 13:54:34 2015 +0100
    14.3 @@ -22,7 +22,7 @@
    14.4  
    14.5        val request =
    14.6          Event_Timer.request (Time.+ (Time.now (), timeout))
    14.7 -          (fn () => Simple_Thread.interrupt_unsynchronized self);
    14.8 +          (fn () => Standard_Thread.interrupt_unsynchronized self);
    14.9  
   14.10        val result =
   14.11          Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
    15.1 --- a/src/Pure/GUI/gui_thread.scala	Tue Nov 03 11:24:42 2015 +0100
    15.2 +++ b/src/Pure/GUI/gui_thread.scala	Tue Nov 03 13:54:34 2015 +0100
    15.3 @@ -50,8 +50,8 @@
    15.4    /* delayed events */
    15.5  
    15.6    def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
    15.7 -    : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
    15.8 +    : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
    15.9  
   15.10    def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
   15.11 -    : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
   15.12 +    : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
   15.13  }
    16.1 --- a/src/Pure/PIDE/prover.scala	Tue Nov 03 11:24:42 2015 +0100
    16.2 +++ b/src/Pure/PIDE/prover.scala	Tue Nov 03 13:54:34 2015 +0100
    16.3 @@ -122,7 +122,7 @@
    16.4    /** process manager **/
    16.5  
    16.6    private val (_, process_result) =
    16.7 -    Simple_Thread.future("process_result") { system_process.join }
    16.8 +    Standard_Thread.future("process_result") { system_process.join }
    16.9  
   16.10    private def terminate_process()
   16.11    {
   16.12 @@ -132,7 +132,7 @@
   16.13      }
   16.14    }
   16.15  
   16.16 -  private val process_manager = Simple_Thread.fork("process_manager")
   16.17 +  private val process_manager = Standard_Thread.fork("process_manager")
   16.18    {
   16.19      val (startup_failed, startup_errors) =
   16.20      {
   16.21 @@ -230,7 +230,7 @@
   16.22        if (err) ("standard_error", system_process.stderr, Markup.STDERR)
   16.23        else ("standard_output", system_process.stdout, Markup.STDOUT)
   16.24  
   16.25 -    Simple_Thread.fork(name) {
   16.26 +    Standard_Thread.fork(name) {
   16.27        try {
   16.28          var result = new StringBuilder(100)
   16.29          var finished = false
   16.30 @@ -268,7 +268,7 @@
   16.31      class Protocol_Error(msg: String) extends Exception(msg)
   16.32  
   16.33      val name = "message_output"
   16.34 -    Simple_Thread.fork(name) {
   16.35 +    Standard_Thread.fork(name) {
   16.36        val default_buffer = new Array[Byte](65536)
   16.37        var c = -1
   16.38  
    17.1 --- a/src/Pure/PIDE/session.scala	Tue Nov 03 11:24:42 2015 +0100
    17.2 +++ b/src/Pure/PIDE/session.scala	Tue Nov 03 13:54:34 2015 +0100
    17.3 @@ -291,7 +291,7 @@
    17.4        nodes = Set.empty
    17.5        commands = Set.empty
    17.6      }
    17.7 -    private val delay_flush = Simple_Thread.delay_first(output_delay) { flush() }
    17.8 +    private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
    17.9  
   17.10      def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
   17.11        assignment |= assign
   17.12 @@ -353,7 +353,7 @@
   17.13  
   17.14    /* manager thread */
   17.15  
   17.16 -  private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
   17.17 +  private val delay_prune = Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
   17.18  
   17.19    private val manager: Consumer_Thread[Any] =
   17.20    {
    18.1 --- a/src/Pure/ROOT	Tue Nov 03 11:24:42 2015 +0100
    18.2 +++ b/src/Pure/ROOT	Tue Nov 03 13:54:34 2015 +0100
    18.3 @@ -86,9 +86,9 @@
    18.4      "Concurrent/par_list.ML"
    18.5      "Concurrent/par_list_sequential.ML"
    18.6      "Concurrent/random.ML"
    18.7 -    "Concurrent/simple_thread.ML"
    18.8      "Concurrent/single_assignment.ML"
    18.9      "Concurrent/single_assignment_sequential.ML"
   18.10 +    "Concurrent/standard_thread.ML"
   18.11      "Concurrent/synchronized.ML"
   18.12      "Concurrent/synchronized_sequential.ML"
   18.13      "Concurrent/task_queue.ML"
    19.1 --- a/src/Pure/ROOT.ML	Tue Nov 03 11:24:42 2015 +0100
    19.2 +++ b/src/Pure/ROOT.ML	Tue Nov 03 13:54:34 2015 +0100
    19.3 @@ -109,7 +109,7 @@
    19.4  then use "ML/ml_statistics_polyml-5.5.0.ML"
    19.5  else use "ML/ml_statistics_dummy.ML";
    19.6  
    19.7 -use "Concurrent/simple_thread.ML";
    19.8 +use "Concurrent/standard_thread.ML";
    19.9  
   19.10  use "Concurrent/single_assignment.ML";
   19.11  if Multithreading.available then ()
    20.1 --- a/src/Pure/System/invoke_scala.scala	Tue Nov 03 11:24:42 2015 +0100
    20.2 +++ b/src/Pure/System/invoke_scala.scala	Tue Nov 03 13:54:34 2015 +0100
    20.3 @@ -94,7 +94,7 @@
    20.4      msg.properties match {
    20.5        case Markup.Invoke_Scala(name, id) =>
    20.6          futures += (id ->
    20.7 -          Simple_Thread.submit_task {
    20.8 +          Standard_Thread.submit_task {
    20.9              val (tag, result) = Invoke_Scala.method(name, msg.text)
   20.10              fulfill(prover, id, tag, result)
   20.11            })
    21.1 --- a/src/Pure/System/isabelle_system.scala	Tue Nov 03 11:24:42 2015 +0100
    21.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Nov 03 13:54:34 2015 +0100
    21.3 @@ -329,11 +329,11 @@
    21.4  
    21.5        val limited = new Limited_Progress(proc, progress_limit)
    21.6        val (_, stdout) =
    21.7 -        Simple_Thread.future("bash_stdout") {
    21.8 +        Standard_Thread.future("bash_stdout") {
    21.9            File.read_lines(proc.stdout, limited(progress_stdout))
   21.10          }
   21.11        val (_, stderr) =
   21.12 -        Simple_Thread.future("bash_stderr") {
   21.13 +        Standard_Thread.future("bash_stderr") {
   21.14            File.read_lines(proc.stderr, limited(progress_stderr))
   21.15          }
   21.16  
    22.1 --- a/src/Pure/System/message_channel.ML	Tue Nov 03 11:24:42 2015 +0100
    22.2 +++ b/src/Pure/System/message_channel.ML	Tue Nov 03 13:54:34 2015 +0100
    22.3 @@ -60,11 +60,11 @@
    22.4      let
    22.5        val mbox = Mailbox.create ();
    22.6        val thread =
    22.7 -        Simple_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
    22.8 +        Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
    22.9            (message_output mbox channel);
   22.10        fun send msg = Mailbox.send mbox (SOME msg);
   22.11        fun shutdown () =
   22.12 -        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
   22.13 +        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
   22.14      in Message_Channel {send = send, shutdown = shutdown} end
   22.15    else
   22.16      let
    23.1 --- a/src/Pure/Tools/build.scala	Tue Nov 03 11:24:42 2015 +0100
    23.2 +++ b/src/Pure/Tools/build.scala	Tue Nov 03 13:54:34 2015 +0100
    23.3 @@ -599,7 +599,7 @@
    23.4        }
    23.5  
    23.6      private val (thread, result) =
    23.7 -      Simple_Thread.future("build") {
    23.8 +      Standard_Thread.future("build") {
    23.9          Isabelle_System.bash_env(info.dir.file, env, script,
   23.10            progress_stdout = (line: String) =>
   23.11              Library.try_unprefix("\floading_theory = ", line) match {
    24.1 --- a/src/Pure/Tools/debugger.ML	Tue Nov 03 11:24:42 2015 +0100
    24.2 +++ b/src/Pure/Tools/debugger.ML	Tue Nov 03 13:54:34 2015 +0100
    24.3 @@ -24,7 +24,7 @@
    24.4    if msg = "" then ()
    24.5    else
    24.6      Output.protocol_message
    24.7 -      (Markup.debugger_output (Simple_Thread.the_name ()))
    24.8 +      (Markup.debugger_output (Standard_Thread.the_name ()))
    24.9        [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
   24.10  
   24.11  val writeln_message = output_message Markup.writelnN;
   24.12 @@ -255,7 +255,7 @@
   24.13          (SOME (fn (_, break) =>
   24.14            if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
   24.15            then
   24.16 -            (case Simple_Thread.get_name () of
   24.17 +            (case Standard_Thread.get_name () of
   24.18                SOME thread_name => debugger_loop thread_name
   24.19              | NONE => ())
   24.20            else ()))));
    25.1 --- a/src/Pure/Tools/debugger.scala	Tue Nov 03 11:24:42 2015 +0100
    25.2 +++ b/src/Pure/Tools/debugger.scala	Tue Nov 03 13:54:34 2015 +0100
    25.3 @@ -114,7 +114,7 @@
    25.4    case object Update
    25.5  
    25.6    private val delay_update =
    25.7 -    Simple_Thread.delay_first(global_state.value.session.output_delay) {
    25.8 +    Standard_Thread.delay_first(global_state.value.session.output_delay) {
    25.9        global_state.value.session.debugger_updates.post(Update)
   25.10      }
   25.11  
    26.1 --- a/src/Pure/build-jars	Tue Nov 03 11:24:42 2015 +0100
    26.2 +++ b/src/Pure/build-jars	Tue Nov 03 13:54:34 2015 +0100
    26.3 @@ -16,7 +16,7 @@
    26.4    Concurrent/future.scala
    26.5    Concurrent/mailbox.scala
    26.6    Concurrent/par_list.scala
    26.7 -  Concurrent/simple_thread.scala
    26.8 +  Concurrent/standard_thread.scala
    26.9    Concurrent/synchronized.scala
   26.10    GUI/color_value.scala
   26.11    GUI/gui.scala
    27.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 11:24:42 2015 +0100
    27.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 13:54:34 2015 +0100
    27.3 @@ -130,7 +130,7 @@
    27.4  
    27.5        future_refresh.map(_.cancel(true))
    27.6        future_refresh =
    27.7 -        Some(Simple_Thread.submit_task {
    27.8 +        Some(Standard_Thread.submit_task {
    27.9            val (text, rendering) =
   27.10              try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
   27.11              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
    28.1 --- a/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 11:24:42 2015 +0100
    28.2 +++ b/src/Tools/jEdit/src/session_build.scala	Tue Nov 03 13:54:34 2015 +0100
    28.3 @@ -161,7 +161,7 @@
    28.4      setLocationRelativeTo(view)
    28.5      setVisible(true)
    28.6  
    28.7 -    Simple_Thread.fork("session_build") {
    28.8 +    Standard_Thread.fork("session_build") {
    28.9        progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
   28.10  
   28.11        val (out, rc) =
    29.1 --- a/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 11:24:42 2015 +0100
    29.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 13:54:34 2015 +0100
    29.3 @@ -128,7 +128,7 @@
    29.4              }
    29.5  
    29.6              future_refresh =
    29.7 -              Some(Simple_Thread.submit_task {
    29.8 +              Some(Standard_Thread.submit_task {
    29.9                  val line_count = overview.line_count
   29.10                  val char_count = overview.char_count
   29.11                  val L = overview.L