# HG changeset patch
# User wenzelm
# Date 1754856710 -7200
# Node ID cbeab5584c62131f44ccaa14c30dfab6500f92a8
# Parent  4629fcbf53e23c72a551acdcb9d959777a257ba9
tuned signature: more explicit operations;

diff -r 4629fcbf53e2 -r cbeab5584c62 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sun Aug 10 22:07:26 2025 +0200
+++ b/src/Pure/Admin/build_doc.scala	Sun Aug 10 22:11:50 2025 +0200
@@ -39,8 +39,7 @@
 
     progress.echo("Build started for sessions " + commas_quote(selection.sessions))
     val build_results =
-      Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs)
-    if (!build_results.ok) error("Build failed")
+      Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).check
 
     progress.echo("Build started for documentation " + commas_quote(documents))
     val deps = Sessions.load_structure(options + "document").selection_deps(selection)
diff -r 4629fcbf53e2 -r cbeab5584c62 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sun Aug 10 22:07:26 2025 +0200
+++ b/src/Pure/Build/build.scala	Sun Aug 10 22:11:50 2025 +0200
@@ -98,6 +98,11 @@
 
     lazy val unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted
 
+    def check: Results =
+      if (ok) this
+      else if (unfinished.isEmpty) error("Build failed")
+      else error("Build failed with unfinished session(s): " + commas(unfinished))
+
     override def toString: String = rc.toString
   }
 
diff -r 4629fcbf53e2 -r cbeab5584c62 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sun Aug 10 22:07:26 2025 +0200
+++ b/src/Pure/Build/build_benchmark.scala	Sun Aug 10 22:11:50 2025 +0200
@@ -34,8 +34,7 @@
     val options1 = options.string.update("build_engine", Build.Engine.Default.name)
     val selection =
       Sessions.Selection(requirements = true, sessions = List(benchmark_session(options)))
-    val res = Build.build(options1, selection = selection, progress = progress, build_heap = true)
-    if (!res.ok) error("Failed building requirements")
+    Build.build(options1, selection = selection, progress = progress, build_heap = true).check
   }
 
   def run_benchmark(options: Options, progress: Progress = new Progress): Unit = {
diff -r 4629fcbf53e2 -r cbeab5584c62 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Aug 10 22:07:26 2025 +0200
+++ b/src/Pure/Thy/document_build.scala	Sun Aug 10 22:11:50 2025 +0200
@@ -597,8 +597,7 @@
         progress.interrupt_handler {
           val build_results =
             Build.build(options, selection = Sessions.Selection.session(session),
-              dirs = dirs, progress = progress)
-          if (!build_results.ok) error("Failed to build session " + quote(session))
+              dirs = dirs, progress = progress).check
 
           if (output_sources.isEmpty && output_pdf.isEmpty) {
             progress.echo_warning("No output directory")