# HG changeset patch
# User wenzelm
# Date 1689952648 -7200
# Node ID 103a81e60126af8a7e10c7ac70f1b023a50b003a
# Parent  48cbee2a6f2ed6d8345bf1712e25bec7c653dda2
tuned signature: more options;

diff -r 48cbee2a6f2e -r 103a81e60126 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Fri Jul 21 17:06:53 2023 +0200
+++ b/src/Pure/Concurrent/par_list.scala	Fri Jul 21 17:17:28 2023 +0200
@@ -12,7 +12,8 @@
   def managed_results[A, B](
     f: A => B,
     xs: List[A],
-    sequential: Boolean = false
+    sequential: Boolean = false,
+    thread: Boolean = false
   ) : List[Exn.Result[B]] = {
     if (sequential || xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
     else {
@@ -30,12 +31,13 @@
       try {
         state.change(_ =>
           (xs.iterator.zipWithIndex.map({ case (x, self) =>
-            Future.fork {
+            def run =
               Exn.capture { f(x) } match {
                 case Exn.Exn(exn) => cancel_other(self); throw exn
                 case Exn.Res(res) => res
               }
-            }
+            if (thread) Future.thread("Par_List.managed_results") { run }
+            else Future.fork { run }
           }).toList, false))
 
         state.value._1.map(_.join_result)
@@ -44,8 +46,12 @@
     }
   }
 
-  def map[A, B](f: A => B, xs: List[A], sequential: Boolean = false): List[B] =
-    Exn.release_first(managed_results(f, xs, sequential = sequential))
+  def map[A, B](f: A => B, xs: List[A],
+    sequential: Boolean = false,
+    thread: Boolean = false
+  ): List[B] = {
+    Exn.release_first(managed_results(f, xs, sequential = sequential, thread = thread))
+  }
 
   private class Found(val res: Any) extends Exception