# HG changeset patch
# User wenzelm
# Date 1676287037 -3600
# Node ID 9cb8fb31e245e59dffb40b880e2b6bdde5b1ac87
# Parent  f7e413e8d2698711fdef5845f3a4a7afe7d4334d
clarified signature: more explicit synchronized operations;

diff -r f7e413e8d269 -r 9cb8fb31e245 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 12:00:21 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 12:17:17 2023 +0100
@@ -190,6 +190,15 @@
       Set.from(for { job <- _running.valuesIterator; i <- job.numa_node } yield i))
   }
 
+  private def job_running(name: String, job: Build_Job): Build_Job = synchronized {
+    _running += (name -> job)
+    job
+  }
+
+  private def remove_running(name: String): Unit = synchronized {
+    _running -= name
+  }
+
   private def session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
@@ -255,7 +264,7 @@
 
     synchronized {
       remove_pending(session_name)
-      _running -= session_name
+      remove_running(session_name)
       _results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail))
     }
   }
@@ -320,11 +329,9 @@
       val job =
         synchronized {
           val numa_node = next_numa_node()
-          val job =
+          job_running(session_name,
             new Build_Job(progress, session_background, store, do_store,
-              resources, session_setup, input_heaps, numa_node)
-          _running += (session_name -> job)
-          job
+              resources, session_setup, input_heaps, numa_node))
         }
       job.start()
     }