# HG changeset patch
# User wenzelm
# Date 1676291203 -3600
# Node ID eeaa2872320bd6f08c63d7d24e3abacf966dbde5
# Parent  ab13ac27c74a0dbe6f35b1f3cc177fd483260b13
clarified signature: more explicit synchronized operations;

diff -r ab13ac27c74a -r eeaa2872320b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 12:47:55 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 13:26:43 2023 +0100
@@ -180,9 +180,12 @@
   }
 
   private def next_pending(): Option[String] = synchronized {
-    _build_order.iterator
-      .dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name))
-      .nextOption()
+    if (_running.size < (max_jobs max 1)) {
+      _build_order.iterator
+        .dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name))
+        .nextOption()
+    }
+    else None
   }
 
   private def next_numa_node(): Option[Int] = synchronized {
@@ -194,6 +197,10 @@
 
   private def stop_running(): Unit = synchronized { _running.valuesIterator.foreach(_.terminate()) }
 
+  private def finished_running(): List[Build_Job] = synchronized {
+    _running.valuesIterator.filter(_.is_finished).toList
+  }
+
   private def job_running(name: String, job: Build_Job): Build_Job = synchronized {
     _running += (name -> job)
     job
@@ -226,7 +233,8 @@
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
-  private def finish_job(session_name: String, job: Build_Job): Unit = {
+  private def finish_job(job: Build_Job): Unit = {
+    val session_name = job.session_name
     val process_result = job.join
     val output_heap = job.finish
 
@@ -366,13 +374,10 @@
     while (test_running()) {
       if (progress.stopped) stop_running()
 
-      synchronized { _running } .find({ case (_, job) => job.is_finished }) match {
-        case Some((session_name, job)) => finish_job(session_name, job)
-        case None if synchronized { _running.size } < (max_jobs max 1) =>
-          next_pending() match {
-            case Some(session_name) => start_job(session_name)
-            case None => sleep()
-          }
+      for (job <- finished_running()) finish_job(job)
+
+      next_pending() match {
+        case Some(session_name) => start_job(session_name)
         case None => sleep()
       }
     }