--- a/src/Pure/Tools/build.scala Sun Feb 19 13:51:49 2023 +0100
+++ b/src/Pure/Tools/build.scala Mon Feb 20 10:29:45 2023 +0100
@@ -132,33 +132,23 @@
}
val results = {
- val build_results =
- if (build_deps.is_empty) {
- progress.echo_warning("Nothing to build")
- Map.empty[String, Build_Process.Result]
- }
- else {
- 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 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 <- build_results.get(name)
+ result <- process_results.get(name)
if result.ok
} yield name).toList
- val results =
- (for ((name, result) <- build_results.iterator)
- yield (name, result.process_result)).toMap
-
- new Results(store, build_deps, sessions_ok, results)
+ new Results(store, build_deps, sessions_ok, process_results)
}
if (export_files) {
--- a/src/Pure/Tools/build_process.scala Sun Feb 19 13:51:49 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Feb 20 10:29:45 2023 +0100
@@ -374,18 +374,25 @@
build_options.seconds("editor_input_delay").sleep()
}
- def run(): Map[String, Build_Process.Result] = {
- while (test_running()) {
- if (progress.stopped) stop_running()
+ def run(): Map[String, Process_Result] = {
+ if (test_running()) {
+ while (test_running()) {
+ if (progress.stopped) stop_running()
+
+ for (job <- finished_running()) finish_job(job)
- for (job <- finished_running()) finish_job(job)
-
- next_pending() match {
- case Some(session_name) => start_job(session_name)
- case None => sleep()
+ next_pending() match {
+ case Some(session_name) => start_job(session_name)
+ case None => sleep()
+ }
+ }
+ synchronized {
+ for ((name, result) <- _results) yield name -> result.process_result
}
}
-
- synchronized { _results }
+ else {
+ progress.echo_warning("Nothing to build")
+ Map.empty[String, Process_Result]
+ }
}
}