--- 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)) }