clarified signature;
authorwenzelm
Mon, 20 Feb 2023 11:38:21 +0100
changeset 77314 22564364274e
parent 77313 f8aa1647d156
child 77315 f34559b24277
clarified signature;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 20 11:34:31 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 20 11:38:21 2023 +0100
@@ -190,6 +190,8 @@
   private var _running = Map.empty[String, Build_Job]
   private var _results = Map.empty[String, Build_Process.Result]
 
+  private def test_pending(): Boolean = synchronized { _pending.nonEmpty }
+
   private def remove_pending(name: String): Unit = synchronized {
     _pending = _pending.flatMap(entry => if (entry.name == name) None else Some(entry.resolve(name)))
   }
@@ -208,8 +210,6 @@
       Set.from(for { job <- _running.valuesIterator; i <- job.numa_node } yield i))
   }
 
-  private def test_running(): Boolean = synchronized { _pending.nonEmpty }
-
   private def stop_running(): Unit = synchronized { _running.valuesIterator.foreach(_.terminate()) }
 
   private def finished_running(): List[Build_Job.Build_Session] = synchronized {
@@ -380,8 +380,8 @@
     }
 
   def run(): Map[String, Process_Result] = {
-    if (test_running()) {
-      while (test_running()) {
+    if (test_pending()) {
+      while (test_pending()) {
         if (progress.stopped) stop_running()
 
         for (job <- finished_running()) finish_job(job)