# HG changeset patch
# User wenzelm
# Date 1677699422 -3600
# Node ID 7a52ba76aa9e0176f2342fdbe843fc7748c36443
# Parent  403748b23f13eb9d7ae4c50cdaa3ab86d78c860d
tuned signature;

diff -r 403748b23f13 -r 7a52ba76aa9e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 20:21:09 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 20:37:02 2023 +0100
@@ -103,9 +103,7 @@
   ) {
     def sessions_structure: Sessions.Structure = build_deps.sessions_structure
 
-    def session_context(session: String): Build_Job.Session_Context = sessions(session)
-
-    def sources_shasum(session: String): SHA1.Shasum = session_context(session).sources_shasum
+    def sources_shasum(session: String): SHA1.Shasum = sessions(session).sources_shasum
 
     def old_command_timings(session: String): List[Properties.T] =
       sessions.get(session) match {
@@ -555,7 +553,7 @@
 
   protected def start_job(session_name: String): Unit = {
     val ancestor_results = synchronized {
-      _state.get_results(build_context.session_context(session_name).ancestors)
+      _state.get_results(build_context.sessions(session_name).ancestors)
     }
     val input_heaps =
       if (ancestor_results.isEmpty) {