# HG changeset patch
# User wenzelm
# Date 1676885385 -3600
# Node ID 6754b5eceb124208b6dc7eb8305e3934f2a84b21
# Parent  632a92fcb6730b72a802d793829d69410b2fcf94
clarified modules;
clarified signature;

diff -r 632a92fcb673 -r 6754b5eceb12 src/Pure/Tools/build.scala
--- 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) {
diff -r 632a92fcb673 -r 6754b5eceb12 src/Pure/Tools/build_process.scala
--- 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]
+    }
   }
 }