--- a/src/Pure/Admin/build_doc.scala Thu Nov 12 12:10:17 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Thu Nov 12 12:34:36 2020 +0100
@@ -46,10 +46,21 @@
val doc_options =
options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
val deps = Sessions.load_structure(doc_options).selection_deps(selection)
- for (session <- selection.sessions) {
- progress.expose_interrupt()
- Present.build_documents(session, deps, store, progress = progress)
- }
+
+ val errs =
+ Par_List.map((doc_session: (String, String)) =>
+ try {
+ progress.expose_interrupt()
+ Present.build_documents(doc_session._2, deps, store, progress = progress)
+ None
+ }
+ catch {
+ case Exn.Interrupt.ERROR(msg) =>
+ val sep = if (msg.contains('\n')) "\n" else " "
+ Some("Documentation " + doc_session._1 + " failed:" + sep + msg)
+ }, selected).flatten
+
+ if (errs.nonEmpty) error(cat_lines(errs))
}