--- 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))
--- 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] = {