--- a/src/Pure/Concurrent/future.scala Sat Apr 04 20:53:36 2020 +0200
+++ b/src/Pure/Concurrent/future.scala Sat Apr 04 21:16:06 2020 +0200
@@ -17,8 +17,17 @@
def value[A](x: A): Future[A] = new Value_Future(x)
def fork[A](body: => A): Future[A] = new Task_Future[A](body)
def promise[A]: Promise[A] = new Promise_Future[A]
- def thread[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
- new Thread_Future[A](name, daemon, body)
+
+ def thread[A](
+ name: String = "",
+ group: ThreadGroup = Standard_Thread.current_thread_group,
+ pri: Int = Thread.NORM_PRIORITY,
+ daemon: Boolean = false,
+ inherit_locals: Boolean = false,
+ uninterruptible: Boolean = false)(body: => A): Future[A] =
+ {
+ new Thread_Future[A](name, group, pri, daemon, inherit_locals, uninterruptible, body)
+ }
}
trait Future[A]
@@ -131,11 +140,20 @@
/* thread future */
-private class Thread_Future[A](name: String, daemon: Boolean, body: => A) extends Future[A]
+private class Thread_Future[A](
+ name: String,
+ group: ThreadGroup,
+ pri: Int,
+ daemon: Boolean,
+ inherit_locals: Boolean,
+ uninterruptible: Boolean,
+ body: => A) extends Future[A]
{
private val result = Future.promise[A]
private val thread =
- Standard_Thread.fork(name = name, daemon = daemon) { result.fulfill_result(Exn.capture(body)) }
+ Standard_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
+ inherit_locals = inherit_locals, uninterruptible = uninterruptible)
+ { result.fulfill_result(Exn.capture(body)) }
def peek: Option[Exn.Result[A]] = result.peek
def join_result: Exn.Result[A] = result.join_result
--- a/src/Pure/Concurrent/standard_thread.scala Sat Apr 04 20:53:36 2020 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala Sat Apr 04 21:16:06 2020 +0200
@@ -26,9 +26,12 @@
group: ThreadGroup = current_thread_group,
pri: Int = Thread.NORM_PRIORITY,
daemon: Boolean = false,
- inherit_locals: Boolean = false)(body: => Unit): Standard_Thread =
+ inherit_locals: Boolean = false,
+ uninterruptible: Boolean = false)(body: => Unit): Standard_Thread =
{
- val main = new Runnable { override def run { body } }
+ val main =
+ if (uninterruptible) new Runnable { override def run { body } }
+ else new Runnable { override def run { Standard_Thread.uninterruptible { body } } }
val thread =
new Standard_Thread(main, name = make_name(name = name), group = group,
pri = pri, daemon = daemon, inherit_locals = inherit_locals)