# HG changeset patch
# User wenzelm
# Date 1726493975 -7200
# Node ID 42ab8c52067e5b528a87c393a3256a8bbdbdd66f
# Parent  f097ca0989e0a243a5665d925f18fcd53c1ab63c
clarified signature;

diff -r f097ca0989e0 -r 42ab8c52067e src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Mon Sep 16 14:03:25 2024 +0200
+++ b/src/Pure/Admin/build_doc.scala	Mon Sep 16 15:39:35 2024 +0200
@@ -46,7 +46,7 @@
     val deps = Sessions.load_structure(options + "document").selection_deps(selection)
 
     val errs =
-      Par_List.map[(String, String), Option[String]](
+      Par_List.maps[(String, String), String](
       {
         case (doc, session) =>
           try {
@@ -66,7 +66,7 @@
               val sep = if (msg.contains('\n')) "\n" else " "
               Some("Documentation " + quote(doc) + " failed:" + sep + msg)
           }
-      }, selected, sequential = sequential).flatten
+      }, selected, sequential = sequential)
 
     if (errs.nonEmpty) error(cat_lines(errs))
 
diff -r f097ca0989e0 -r 42ab8c52067e 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] = {