clarified signature: prefer static data;

--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 19:48:19 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 20:21:09 2023 +0100
@@ -44,12 +44,13 @@
       name: String,
       deps: List[String],
       ancestors: List[String],
+      sources_shasum: SHA1.Shasum,
       timeout: Time,
       store: Sessions.Store,
       progress: Progress = new Progress
     ): Session_Context = {
       def default: Session_Context =
-        new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty)
+        new Session_Context(name, deps, ancestors, sources_shasum, timeout, Time.zero, Bytes.empty)
 
       store.try_open_database(name) match {
         case None => default
@@ -68,7 +69,7 @@
                 case _ => Time.zero
               }
             new Session_Context(
-              name, deps, ancestors, timeout, elapsed, command_timings)
+              name, deps, ancestors, sources_shasum, timeout, elapsed, command_timings)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -84,6 +85,7 @@
     val name: String,
     val deps: List[String],
     val ancestors: List[String],
+    val sources_shasum: SHA1.Shasum,
     val timeout: Time,
     val old_time: Time,
     val old_command_timings_blob: Bytes
@@ -97,7 +99,6 @@
     session_heaps: List[Path],
     do_store: Boolean,
     resources: Resources,
-    sources_shasum: SHA1.Shasum,
     input_heaps: SHA1.Shasum,
     override val node_info: Node_Info
   ) extends Build_Job {
@@ -470,7 +471,9 @@
           build_log =
             if (process_result.timeout) build_log.error("Timeout") else build_log,
           build =
-            Sessions.Build_Info(sources_shasum, input_heaps, output_heap,
+            Sessions.Build_Info(
+              sources = build_context.sources_shasum(session_name),
+              input_heaps = input_heaps, output_heap = output_heap,
               process_result.rc, build_context.uuid)))
 
       // messages

--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 19:48:19 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 20:21:09 2023 +0100
@@ -39,9 +39,10 @@
           yield {
             val deps = info.parent.toList
             val ancestors = sessions_structure.build_requirements(deps)
+            val sources_shasum = build_deps.sources_shasum(name)
             val session_context =
               Build_Job.Session_Context.load(
-                name, deps, ancestors, info.timeout, store, progress = progress)
+                name, deps, ancestors, sources_shasum, info.timeout, store, progress = progress)
             name -> session_context
           })
 
@@ -104,6 +105,8 @@
 
     def session_context(session: String): Build_Job.Session_Context = sessions(session)
 
+    def sources_shasum(session: String): SHA1.Shasum = session_context(session).sources_shasum
+
     def old_command_timings(session: String): List[Properties.T] =
       sessions.get(session) match {
         case Some(session_context) =>
@@ -570,7 +573,7 @@
               val current =
                 !build_context.fresh_build &&
                 build.ok &&
-                build.sources == build_deps.sources_shasum(session_name) &&
+                build.sources == build_context.sources_shasum(session_name) &&
                 build.input_heaps == input_heaps &&
                 build.output_heap == output_heap &&
                 !(do_store && output_heap.is_empty)
@@ -629,7 +632,7 @@
           val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
           val job =
             new Build_Job.Session_Job(build_context, session_background, session_heaps,
-              do_store, resources, build_deps.sources_shasum(session_name), input_heaps, node_info)
+              do_store, resources, input_heaps, node_info)
           _state = state1.add_running(session_name, job)
           job
         }