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