# HG changeset patch
# User wenzelm
# Date 1676886127 -3600
# Node ID 5212446f3d7f8a4e2b539568641e9a1cf3fc3f69
# Parent  6754b5eceb124208b6dc7eb8305e3934f2a84b21
clarified signature;

diff -r 6754b5eceb12 -r 5212446f3d7f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Feb 20 10:29:45 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 20 10:42:07 2023 +0100
@@ -11,14 +11,24 @@
 object Build {
   /** build with results **/
 
-  class Results private[Build](
+  object Results {
+    def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results =
+      new Results(context.store, context.deps, results)
+  }
+
+  class Results private(
     val store: Sessions.Store,
     val deps: Sessions.Deps,
-    val sessions_ok: List[String],
     results: Map[String, Process_Result]
   ) {
     def cache: Term.Cache = store.cache
 
+    def sessions_ok: List[String] =
+      (for {
+        name <- deps.sessions_structure.build_topological_order.iterator
+        result <- results.get(name) if result.ok
+      } yield name).toList
+
     def info(name: String): Sessions.Info = deps.sessions_structure(name)
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = !results(name).defined
@@ -131,25 +141,14 @@
       }
     }
 
-    val results = {
-      val process_results =
-        Isabelle_Thread.uninterruptible {
-          val build_process =
-            new Build_Process(build_context, build_heap = build_heap,
-              numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
-              no_build = no_build, verbose = verbose, session_setup = session_setup)
-          build_process.run()
-        }
-
-      val sessions_ok: List[String] =
-        (for {
-          name <- build_deps.sessions_structure.build_topological_order.iterator
-          result <- process_results.get(name)
-          if result.ok
-        } yield name).toList
-
-      new Results(store, build_deps, sessions_ok, process_results)
-    }
+    val results =
+      Isabelle_Thread.uninterruptible {
+        val build_process =
+          new Build_Process(build_context, build_heap = build_heap,
+            numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
+            no_build = no_build, verbose = verbose, session_setup = session_setup)
+        Results(build_context, build_process.run())
+      }
 
     if (export_files) {
       for (name <- full_sessions_selection.iterator if results(name).ok) {