# HG changeset patch
# User wenzelm
# Date 1586084740 -7200
# Node ID f8e52c0152fe37e1021c6900d1b53011ba8651f1
# Parent  d682b4000a77318f114134f4be29ca9bcc22c091
clarified names;

diff -r d682b4000a77 -r f8e52c0152fe src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -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),
-      Standard_Thread.attributes
+      Isabelle_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 (Standard_Thread.interrupt_unsynchronized o #1) canceling
+                val _ = List.app (Isabelle_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 d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -47,7 +47,7 @@
   private var active = true
   private val mailbox = Mailbox[Option[Request]]
 
-  private val thread = Standard_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
+  private val thread = Isabelle_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
   def is_active: Boolean = active && thread.isAlive
   def check_thread: Boolean = Thread.currentThread == thread
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -130,7 +130,7 @@
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
   else
-    SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
+    SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
       manager_loop);
 
 fun shutdown () =
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -202,14 +202,14 @@
   let
     val running = Task_Queue.cancel (! queue) group;
     val _ = running |> List.app (fn thread =>
-      if Standard_Thread.is_self thread then ()
-      else Standard_Thread.interrupt_unsynchronized thread);
+      if Isabelle_Thread.is_self thread then ()
+      else Isabelle_Thread.interrupt_unsynchronized thread);
   in running end;
 
 fun cancel_all () = (*requires SYNCHRONIZED*)
   let
     val (groups, threads) = Task_Queue.cancel_all (! queue);
-    val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
+    val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
   in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -280,7 +280,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 =
-      Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+      Isabelle_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);
@@ -383,7 +383,7 @@
   if scheduler_active () then ()
   else
     scheduler :=
-      SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+      SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
         scheduler_loop));
 
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/future.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -20,7 +20,7 @@
 
   def thread[A](
     name: String = "",
-    group: ThreadGroup = Standard_Thread.current_thread_group,
+    group: ThreadGroup = Isabelle_Thread.current_thread_group,
     pri: Int = Thread.NORM_PRIORITY,
     daemon: Boolean = false,
     inherit_locals: Boolean = false,
@@ -96,7 +96,7 @@
       status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
     }
   }
-  private val task = Standard_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
+  private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
 
   def join_result: Exn.Result[A] =
   {
@@ -151,7 +151,7 @@
 {
   private val result = Future.promise[A]
   private val thread =
-    Standard_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
+    Isabelle_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
       inherit_locals = inherit_locals, uninterruptible = uninterruptible)
     { result.fulfill_result(Exn.capture(body)) }
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/isabelle_thread.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -0,0 +1,76 @@
+(*  Title:      Pure/Concurrent/isabelle_thread.ML
+    Author:     Makarius
+
+Isabelle-specific thread management.
+*)
+
+signature ISABELLE_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 Isabelle_Thread: ISABELLE_THREAD =
+struct
+
+(* self *)
+
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
+
+(* unique name *)
+
+local
+  val name_var = Thread_Data.var () : string Thread_Data.var;
+  val count = Counter.make ();
+in
+
+fun get_name () = Thread_Data.get name_var;
+
+fun the_name () =
+  (case get_name () of
+    NONE => raise Fail "Unknown thread name"
+  | SOME name => name);
+
+fun set_name base =
+  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
+  Thread.MaximumMLStack stack_limit ::
+  Thread_Attributes.convert_attributes
+    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+
+fun fork (params: params) body =
+  Thread.fork (fn () =>
+    Exn.trace General.exnMessage tracing (fn () =>
+      (set_name (#name params); body ())
+        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.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 d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/isabelle_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -0,0 +1,169 @@
+/*  Title:      Pure/Concurrent/isabelle_thread.scala
+    Author:     Makarius
+
+Isabelle-specific thread management.
+*/
+
+package isabelle
+
+
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
+
+
+object Isabelle_Thread
+{
+  /* fork */
+
+  private val counter = Counter.make()
+
+  def make_name(name: String = "", base: String = "thread"): String =
+    proper_string(name).getOrElse(base + counter())
+
+  def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
+
+  def fork(
+    name: String = "",
+    group: ThreadGroup = current_thread_group,
+    pri: Int = Thread.NORM_PRIORITY,
+    daemon: Boolean = false,
+    inherit_locals: Boolean = false,
+    uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread =
+  {
+    val main =
+      if (uninterruptible) new Runnable { override def run { Isabelle_Thread.uninterruptible { body } } }
+      else new Runnable { override def run { body } }
+    val thread =
+      new Isabelle_Thread(main, name = make_name(name = name), group = group,
+        pri = pri, daemon = daemon, inherit_locals = inherit_locals)
+    thread.start
+    thread
+  }
+
+
+  /* self */
+
+  def self: Isabelle_Thread =
+    Thread.currentThread match {
+      case thread: Isabelle_Thread => thread
+      case _ => error("Expected to run on Isabelle/Scala standard thread")
+    }
+
+  def uninterruptible[A](body: => A): A = self.uninterruptible(body)
+
+
+  /* pool */
+
+  lazy val pool: ThreadPoolExecutor =
+    {
+      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+      val executor =
+        new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+      executor.setThreadFactory(
+        new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
+      executor
+    }
+
+
+  /* delayed events */
+
+  final class Delay private[Isabelle_Thread](
+    first: Boolean, delay: => Time, log: Logger, 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) {
+        try { event }
+        catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+      }
+    }
+
+    def invoke(): Unit = synchronized
+    {
+      val new_run =
+        running match {
+          case Some(request) => if (first) false else { request.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; running = None
+        case None =>
+      }
+    }
+
+    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) {
+            running = Some(Event_Timer.request(alt_time)(run))
+          }
+        case None =>
+      }
+    }
+  }
+
+  // delayed event after first invocation
+  def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
+    new Delay(true, delay, log, event)
+
+  // delayed event after last invocation
+  def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
+    new Delay(false, delay, log, event)
+}
+
+class Isabelle_Thread private(
+    main: Runnable,
+    name: String = "",
+    group: ThreadGroup = null,
+    pri: Int = Thread.NORM_PRIORITY,
+    daemon: Boolean = false,
+    inherit_locals: Boolean = false)
+  extends Thread(group, null, name, 0L, inherit_locals)
+{
+  thread =>
+
+  thread.setPriority(pri)
+  thread.setDaemon(daemon)
+
+  override def run { main.run() }
+
+  private var interruptible: Boolean = true
+  private var interrupt_pending: Boolean = false
+
+  override def interrupt: Unit = synchronized
+  {
+    if (interruptible) super.interrupt()
+    else { interrupt_pending = true }
+  }
+
+  def uninterruptible[A](body: => A): A =
+  {
+    require(Thread.currentThread == thread)
+
+    val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
+    try { body }
+    finally {
+      synchronized {
+        interruptible = interruptible0
+        if (interruptible && interrupt_pending) {
+          interrupt_pending = false
+          super.interrupt()
+        }
+      }
+      Exn.Interrupt.expose()
+    }
+  }
+}
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/standard_thread.ML
--- a/src/Pure/Concurrent/standard_thread.ML	Sat Apr 04 21:38:20 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(*  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 name_var = Thread_Data.var () : string Thread_Data.var;
-  val count = Counter.make ();
-in
-
-fun get_name () = Thread_Data.get name_var;
-
-fun the_name () =
-  (case get_name () of
-    NONE => raise Fail "Unknown thread name"
-  | SOME name => name);
-
-fun set_name base =
-  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
-
-end;
-
-
-(* fork *)
-
-type params = {name: string, stack_limit: int option, interrupts: bool};
-
-fun attributes ({stack_limit, interrupts, ...}: params) =
-  Thread.MaximumMLStack stack_limit ::
-  Thread_Attributes.convert_attributes
-    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
-
-fun fork (params: params) body =
-  Thread.fork (fn () =>
-    Exn.trace General.exnMessage tracing (fn () =>
-      (set_name (#name params); body ())
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.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 d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Sat Apr 04 21:38:20 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,169 +0,0 @@
-/*  Title:      Pure/Concurrent/standard_thread.scala
-    Author:     Makarius
-
-Standard thread operations.
-*/
-
-package isabelle
-
-
-import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
-
-
-object Standard_Thread
-{
-  /* fork */
-
-  private val counter = Counter.make()
-
-  def make_name(name: String = "", base: String = "thread"): String =
-    proper_string(name).getOrElse(base + counter())
-
-  def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
-
-  def fork(
-    name: String = "",
-    group: ThreadGroup = current_thread_group,
-    pri: Int = Thread.NORM_PRIORITY,
-    daemon: Boolean = false,
-    inherit_locals: Boolean = false,
-    uninterruptible: Boolean = false)(body: => Unit): Standard_Thread =
-  {
-    val main =
-      if (uninterruptible) new Runnable { override def run { Standard_Thread.uninterruptible { body } } }
-      else new Runnable { override def run { body } }
-    val thread =
-      new Standard_Thread(main, name = make_name(name = name), group = group,
-        pri = pri, daemon = daemon, inherit_locals = inherit_locals)
-    thread.start
-    thread
-  }
-
-
-  /* self */
-
-  def self: Standard_Thread =
-    Thread.currentThread match {
-      case thread: Standard_Thread => thread
-      case _ => error("Expected to run on Isabelle/Scala standard thread")
-    }
-
-  def uninterruptible[A](body: => A): A = self.uninterruptible(body)
-
-
-  /* pool */
-
-  lazy val pool: ThreadPoolExecutor =
-    {
-      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
-      val executor =
-        new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
-      executor.setThreadFactory(
-        new Standard_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
-      executor
-    }
-
-
-  /* delayed events */
-
-  final class Delay private[Standard_Thread](
-    first: Boolean, delay: => Time, log: Logger, 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) {
-        try { event }
-        catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
-      }
-    }
-
-    def invoke(): Unit = synchronized
-    {
-      val new_run =
-        running match {
-          case Some(request) => if (first) false else { request.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; running = None
-        case None =>
-      }
-    }
-
-    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) {
-            running = Some(Event_Timer.request(alt_time)(run))
-          }
-        case None =>
-      }
-    }
-  }
-
-  // delayed event after first invocation
-  def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
-    new Delay(true, delay, log, event)
-
-  // delayed event after last invocation
-  def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
-    new Delay(false, delay, log, event)
-}
-
-class Standard_Thread private(
-    main: Runnable,
-    name: String = "",
-    group: ThreadGroup = null,
-    pri: Int = Thread.NORM_PRIORITY,
-    daemon: Boolean = false,
-    inherit_locals: Boolean = false)
-  extends Thread(group, null, name, 0L, inherit_locals)
-{
-  thread =>
-
-  thread.setPriority(pri)
-  thread.setDaemon(daemon)
-
-  override def run { main.run() }
-
-  private var interruptible: Boolean = true
-  private var interrupt_pending: Boolean = false
-
-  override def interrupt: Unit = synchronized
-  {
-    if (interruptible) super.interrupt()
-    else { interrupt_pending = true }
-  }
-
-  def uninterruptible[A](body: => A): A =
-  {
-    require(Thread.currentThread == thread)
-
-    val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
-    try { body }
-    finally {
-      synchronized {
-        interruptible = interruptible0
-        if (interruptible && interrupt_pending) {
-          interrupt_pending = false
-          super.interrupt()
-        }
-      }
-      Exn.Interrupt.expose()
-    }
-  }
-}
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -24,7 +24,7 @@
 
       val request =
         Event_Timer.request {physical = false} (start + timeout)
-          (fn () => Standard_Thread.interrupt_unsynchronized self);
+          (fn () => Isabelle_Thread.interrupt_unsynchronized self);
       val result =
         Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -58,9 +58,9 @@
 
   /* delayed events */
 
-  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
-    Standard_Thread.delay_first(delay) { later { event } }
+  def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_first(delay) { later { event } }
 
-  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
-    Standard_Thread.delay_last(delay) { later { event } }
+  def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(delay) { later { event } }
 }
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/General/file_watcher.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -84,13 +84,13 @@
 
     /* changed directory entries */
 
-    private val delay_changed = Standard_Thread.delay_last(delay)
+    private val delay_changed = Isabelle_Thread.delay_last(delay)
     {
       val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
       handle(changed)
     }
 
-    private val watcher_thread = Standard_Thread.fork(name = "file_watcher", daemon = true)
+    private val watcher_thread = Isabelle_Thread.fork(name = "file_watcher", daemon = true)
     {
       try {
         while (true) {
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -304,12 +304,12 @@
       val consumer =
       {
         val delay_nodes_status =
-          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
+          Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) {
             progress.nodes_status(use_theories_state.value.nodes_status)
           }
 
         val delay_commit_clean =
-          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+          Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) {
             val clean_theories = use_theories_state.change_result(_.clean_theories)
             if (clean_theories.nonEmpty) {
               progress.echo("Removing " + clean_theories.length + " theories ...")
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/prover.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -112,7 +112,7 @@
     }
   }
 
-  private val process_manager = Standard_Thread.fork(name = "process_manager")
+  private val process_manager = Isabelle_Thread.fork(name = "process_manager")
   {
     val stdout = physical_output(false)
 
@@ -218,7 +218,7 @@
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
-    Standard_Thread.fork(name = name) {
+    Isabelle_Thread.fork(name = name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
@@ -256,7 +256,7 @@
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
-    Standard_Thread.fork(name = name) {
+    Isabelle_Thread.fork(name = name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -268,7 +268,7 @@
       nodes = Set.empty
       commands = Set.empty
     }
-    private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
+    private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() }
 
     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
       synchronized {
@@ -313,7 +313,7 @@
   private object consolidation
   {
     private val delay =
-      Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+      Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
@@ -382,7 +382,7 @@
   /* manager thread */
 
   private val delay_prune =
-    Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+    Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -117,7 +117,7 @@
 ML_file "ML/ml_statistics.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
-ML_file "Concurrent/standard_thread.ML";
+ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/bash.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -38,7 +38,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+      Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
@@ -86,7 +86,7 @@
           in () end;
 
     fun cleanup () =
-     (Standard_Thread.interrupt_unsynchronized system_thread;
+     (Isabelle_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
   in
     let
@@ -132,7 +132,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+      Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
         Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
@@ -182,7 +182,7 @@
           in () end;
 
     fun cleanup () =
-     (Standard_Thread.interrupt_unsynchronized system_thread;
+     (Isabelle_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
   in
     let
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/command_line.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -26,7 +26,7 @@
   def tool(body: => Unit)
   {
     val thread =
-      Standard_Thread.fork(name = "command_line", inherit_locals = true) {
+      Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
         val rc =
           try { body; 0 }
           catch {
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/message_channel.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -59,11 +59,11 @@
   let
     val mbox = Mailbox.create ();
     val thread =
-      Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+      Isabelle_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
         (message_output mbox stream);
     fun send msg = Mailbox.send mbox (SOME msg);
     fun shutdown () =
-      (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
+      (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Isabelle_Thread.join thread);
   in Message_Channel {send = send, shutdown = shutdown} end;
 
 end;
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/debugger.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -22,7 +22,7 @@
   if msg = "" then ()
   else
     Output.protocol_message
-      (Markup.debugger_output (Standard_Thread.the_name ()))
+      (Markup.debugger_output (Isabelle_Thread.the_name ()))
       [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
 
 val writeln_message = output_message Markup.writelnN;
@@ -250,7 +250,7 @@
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
-            (case Standard_Thread.get_name () of
+            (case Isabelle_Thread.get_name () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/debugger.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -155,7 +155,7 @@
   private val state = Synchronized(Debugger.State())
 
   private val delay_update =
-    Standard_Thread.delay_first(session.output_delay) {
+    Isabelle_Thread.delay_first(session.output_delay) {
       session.debugger_updates.post(Debugger.Update)
     }
 
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/server.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -292,7 +292,7 @@
     val progress: Connection_Progress = context.progress(ident)
     def cancel { progress.stop }
 
-    private lazy val thread = Standard_Thread.fork(name = "server_task")
+    private lazy val thread = Isabelle_Thread.fork(name = "server_task")
     {
       Exn.capture { body(task) } match {
         case Exn.Res(res) =>
@@ -601,12 +601,12 @@
   }
 
   private lazy val server_thread: Thread =
-    Standard_Thread.fork(name = "server") {
+    Isabelle_Thread.fork(name = "server") {
       var finished = false
       while (!finished) {
         Exn.capture(server_socket.accept) match {
           case Exn.Res(socket) =>
-            Standard_Thread.fork(name = "server_connection")
+            Isabelle_Thread.fork(name = "server_connection")
               { using(Server.Connection(socket))(handle) }
           case Exn.Exn(_) => finished = true
         }
diff -r d682b4000a77 -r f8e52c0152fe src/Pure/build-jars
--- a/src/Pure/build-jars	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/build-jars	Sun Apr 05 13:05:40 2020 +0200
@@ -30,9 +30,9 @@
   src/Pure/Concurrent/counter.scala
   src/Pure/Concurrent/event_timer.scala
   src/Pure/Concurrent/future.scala
+  src/Pure/Concurrent/isabelle_thread.scala
   src/Pure/Concurrent/mailbox.scala
   src/Pure/Concurrent/par_list.scala
-  src/Pure/Concurrent/standard_thread.scala
   src/Pure/Concurrent/synchronized.scala
   src/Pure/GUI/color_value.scala
   src/Pure/GUI/gui.scala
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sun Apr 05 13:05:40 2020 +0200
@@ -1715,20 +1715,20 @@
         Just n -> fmap trim_line . fst <$> read_block socket n
 \<close>
 
-generate_file "Isabelle/Standard_Thread.hs" = \<open>
-{-  Title:      Isabelle/Standard_Thread.hs
+generate_file "Isabelle/Isabelle_Thread.hs" = \<open>
+{-  Title:      Isabelle/Isabelle_Thread.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
-Standard thread operations.
-
-See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.ML\<close>
-and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.scala\<close>.
+Isabelle-specific thread management.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\<close>.
 -}
 
 {-# LANGUAGE NamedFieldPuns #-}
 
-module Isabelle.Standard_Thread (
+module Isabelle.Isabelle_Thread (
   ThreadId, Result,
   find_id,
   properties, change_properties,
@@ -1912,7 +1912,7 @@
 import Isabelle.Library
 import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Byte_Message as Byte_Message
-import qualified Isabelle.Standard_Thread as Standard_Thread
+import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
 
 
 {- server address -}
@@ -1953,7 +1953,7 @@
     loop :: Socket -> ByteString -> IO ()
     loop server_socket password = forever $ do
       (connection, _) <- Socket.accept server_socket
-      Standard_Thread.fork_finally
+      Isabelle_Thread.fork_finally
         (do
           line <- Byte_Message.read_line connection
           when (line == Just password) $ handle connection)
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -127,12 +127,12 @@
 
   /* input from client or file-system */
 
-  private val delay_input: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+  private val delay_input: Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { resources.flush_input(session, channel) }
 
-  private val delay_load: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
+  private val delay_load: Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
       val (invoke_input, invoke_load) =
         resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
@@ -183,8 +183,8 @@
 
   /* caret handling */
 
-  private val delay_caret_update: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+  private val delay_caret_update: Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { session.caret_focus.post(Session.Caret_Focus) }
 
   private def update_caret(caret: Option[(JFile, Line.Position)])
@@ -199,8 +199,8 @@
 
   private lazy val preview_panel = new Preview_Panel(resources)
 
-  private lazy val delay_preview: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+  private lazy val delay_preview: Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
       if (preview_panel.flush(channel)) delay_preview.invoke()
     }
@@ -214,8 +214,8 @@
 
   /* output to client */
 
-  private val delay_output: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+  private val delay_output: Isabelle_Thread.Delay =
+    Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
       if (resources.flush_output(channel)) delay_output.invoke()
     }
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/active.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -31,14 +31,14 @@
             // FIXME avoid hard-wired stuff
             elem match {
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                Standard_Thread.fork(name = "browser") {
+                Isabelle_Thread.fork(name = "browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
                   Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
                 }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                Standard_Thread.fork(name = "graphview") {
+                Isabelle_Thread.fork(name = "graphview") {
                   val graph =
                     Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -181,7 +181,7 @@
     if (path.is_file)
       goto_file(true, view, File.platform_path(path))
     else {
-      Standard_Thread.fork(name = "documentation") {
+      Isabelle_Thread.fork(name = "documentation") {
         try { Doc.view(path) }
         catch {
           case exn: Throwable =>
@@ -211,7 +211,7 @@
     new Hyperlink {
       override val external = true
       def follow(view: View): Unit =
-        Standard_Thread.fork(name = "hyperlink_url") {
+        Isabelle_Thread.fork(name = "hyperlink_url") {
           try { Isabelle_System.open(Url.escape_name(name)) }
           catch {
             case exn: Throwable =>
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -154,7 +154,7 @@
         }
         if (required_files.nonEmpty) {
           try {
-            Standard_Thread.fork(name = "resolve_dependencies") {
+            Isabelle_Thread.fork(name = "resolve_dependencies") {
               val loaded_files =
                 for {
                   name <- required_files
diff -r d682b4000a77 -r f8e52c0152fe src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sun Apr 05 13:05:40 2020 +0200
@@ -165,7 +165,7 @@
     setLocationRelativeTo(view)
     setVisible(true)
 
-    Standard_Thread.fork(name = "session_build") {
+    Isabelle_Thread.fork(name = "session_build") {
       progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
 
       val (out, rc) =