src/Pure/Concurrent/par_list.scala

--- a/src/Pure/Concurrent/par_list.scala	Mon Sep 16 14:03:25 2024 +0200
+++ b/src/Pure/Concurrent/par_list.scala	Mon Sep 16 15:39:35 2024 +0200
@@ -46,13 +46,18 @@
     }
   }
 
-  def map[A, B](f: A => B, xs: List[A],
+  def map[A, B](f: A => B, list: List[A],
     sequential: Boolean = false,
     thread: Boolean = false
   ): List[B] = {
-    Exn.release_first(managed_results(f, xs, sequential = sequential, thread = thread))
+    Exn.release_first(managed_results(f, list, sequential = sequential, thread = thread))
   }
 
+  def maps[A, B](f: A => Iterable[B], list: List[A],
+    sequential: Boolean = false,
+    thread: Boolean = false
+  ): List[B] = map(f, list, sequential = sequential, thread = thread).flatten
+
   private class Found(val res: Any) extends Exception
 
   def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] = {