# HG changeset patch # User wenzelm # Date 1676889501 -3600 # Node ID 22564364274e16ed9fd9eca94ee1922104248afb # Parent f8aa1647d156cd0bc43d72425b0559e381c04c4d clarified signature; diff -r f8aa1647d156 -r 22564364274e 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)