# HG changeset patch
# User wenzelm
# Date 1586027766 -7200
# Node ID fef74c06cfacb2bb9f596ea09abbf19bde106472
# Parent  b3f738f12a9a3b0146eba7b2865f3e3231953521
clarified signature;

diff -r b3f738f12a9a -r fef74c06cfac src/Pure/Concurrent/future.scala
--- 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
diff -r b3f738f12a9a -r fef74c06cfac src/Pure/Concurrent/standard_thread.scala
--- 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)