# HG changeset patch
# User wenzelm
# Date 1754681302 -7200
# Node ID ae65438eec0c6914a0e107a2ff6cea82dc83dd14
# Parent  7e8c6cf127f0cd3090a101c9c78d2f58193e7ac4
clarified signature: more detailed result;

diff -r 7e8c6cf127f0 -r ae65438eec0c src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Aug 08 20:34:38 2025 +0200
+++ b/src/Pure/Build/build.scala	Fri Aug 08 21:28:22 2025 +0200
@@ -299,17 +299,27 @@
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false
-  ): Int = {
+  ): Results = {
     val selection = Sessions.Selection.session(logic)
-    val rc =
-      if (!fresh && build(options, selection = selection,
-            build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
+
+    def test_build(): Results =
+      build(options, selection = selection,
+        build_heap = build_heap, no_build = true, dirs = dirs)
+
+    def full_build(): Results = {
+      progress.echo("Build started for Isabelle/" + logic + " ...")
+      build(options, selection = selection, progress = progress,
+        build_heap = build_heap, fresh_build = fresh, dirs = dirs)
+    }
+
+    val results =
+      if (fresh) full_build()
       else {
-        progress.echo("Build started for Isabelle/" + logic + " ...")
-        build(options, selection = selection, progress = progress,
-          build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
+        val results0 = test_build()
+        if (results0.ok) results0 else full_build()
       }
-    if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
+
+    if (strict && !results.ok) error("Failed to build Isabelle/" + logic) else results
   }
 
 
diff -r 7e8c6cf127f0 -r ae65438eec0c src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Fri Aug 08 20:34:38 2025 +0200
+++ b/src/Pure/Build/export.scala	Fri Aug 08 21:28:22 2025 +0200
@@ -659,11 +659,11 @@
         /* build */
 
         if (!no_build) {
-          val rc =
+          val results =
             progress.interrupt_handler {
               Build.build_logic(options, session_name, progress = progress, dirs = dirs)
             }
-          if (rc != Process_Result.RC.ok) sys.exit(rc)
+          if (!results.ok) sys.exit(results.rc)
         }
 
 
diff -r 7e8c6cf127f0 -r ae65438eec0c src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Fri Aug 08 20:34:38 2025 +0200
+++ b/src/Pure/ML/ml_console.scala	Fri Aug 08 21:28:22 2025 +0200
@@ -53,11 +53,11 @@
       // build logic
       if (!no_build && !raw_ml_system) {
         val progress = new Console_Progress()
-        val rc =
+        val results =
           progress.interrupt_handler {
             Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
           }
-        if (rc != Process_Result.RC.ok) sys.exit(rc)
+        if (!results.ok) sys.exit(results.rc)
       }
 
       val session_background =