# HG changeset patch
# User wenzelm
# Date 1677508279 -3600
# Node ID f3e5b3fe230e4f038f4b50335f1bcbf64e7cc59b
# Parent  375c6b9ce9eab7d7e327f8b2fa8fbd3ef10b856c
clarified signature: more explicit "synchronized" regions;

diff -r 375c6b9ce9ea -r f3e5b3fe230e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 27 15:25:46 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 27 15:31:19 2023 +0100
@@ -520,8 +520,6 @@
       (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
         yield Build_Process.Entry(name, preds.toList)).toList)
 
-  protected def finished(): Boolean = synchronized { _state.finished }
-
   protected def next_pending(): Option[String] = synchronized {
     if (_state.running.size < (build_context.max_jobs max 1)) {
       _state.pending.filter(entry => entry.is_ready && !_state.is_running(entry.name))
@@ -531,12 +529,6 @@
     else None
   }
 
-  protected def stop_running(): Unit = synchronized { _state.stop_running() }
-
-  protected def finished_running(): List[Build_Job] = synchronized {
-    _state.finished_running()
-  }
-
   protected def start_job(session_name: String): Unit = {
     val ancestor_results = synchronized {
       _state.get_results(
@@ -645,6 +637,8 @@
     }
 
   def run(): Map[String, Process_Result] = {
+    def finished(): Boolean = synchronized { _state.finished }
+
     if (finished()) {
       progress.echo_warning("Nothing to build")
       Map.empty[String, Process_Result]
@@ -652,9 +646,9 @@
     else {
       setup_database()
       while (!finished()) {
-        if (progress.stopped) stop_running()
+        if (progress.stopped) synchronized { _state.stop_running() }
 
-        for (job <- finished_running()) {
+        for (job <- synchronized { _state.finished_running() }) {
           val job_name = job.job_name
           val (process_result, output_heap) = job.finish
           synchronized {