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

diff -r 9cb8fb31e245 -r 4f4a0c9d2d1a src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 12:17:17 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 12:26:24 2023 +0100
@@ -199,6 +199,15 @@
     _running -= name
   }
 
+  private def add_result(
+    name: String,
+    current: Boolean,
+    output_heap: SHA1.Shasum,
+    process_result: Process_Result
+  ): Unit = synchronized {
+    _results += (name -> Build_Process.Result(current, output_heap, process_result))
+  }
+
   private def session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
@@ -265,7 +274,7 @@
     synchronized {
       remove_pending(session_name)
       remove_running(session_name)
-      _results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail))
+      add_result(session_name, false, output_heap, process_result_tail)
     }
   }
 
@@ -304,14 +313,14 @@
     if (all_current) {
       synchronized {
         remove_pending(session_name)
-        _results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok))
+        add_result(session_name, true, output_heap, Process_Result.ok)
       }
     }
     else if (no_build) {
       progress.echo_if(verbose, "Skipping " + session_name + " ...")
       synchronized {
         remove_pending(session_name)
-        _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error))
+        add_result(session_name, false, output_heap, Process_Result.error)
       }
     }
     else if (ancestor_results.forall(_.ok) && !progress.stopped) {
@@ -339,7 +348,7 @@
       progress.echo(session_name + " CANCELLED")
       synchronized {
         remove_pending(session_name)
-        _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined))
+        add_result(session_name, false, output_heap, Process_Result.undefined)
       }
     }
   }