clarified signature: reduce explicit access to static Sessions.Structure;

--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 14:22:15 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 14:47:20 2023 +0100
@@ -40,32 +40,40 @@
   /* build session */
 
   object Session_Context {
-    def init(session: String, timeout: Time = Time.zero): Session_Context =
-      new Session_Context(session, timeout, Time.zero, Bytes.empty)
+    def init(name: String,
+      deps: List[String],
+      ancestors: List[String],
+      timeout: Time = Time.zero
+    ): Session_Context = new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty)
 
     def load(
-      session: String,
+      name: String,
+      deps: List[String],
+      ancestors: List[String],
       timeout: Time,
       store: Sessions.Store,
       progress: Progress = new Progress
     ): Session_Context = {
-      store.try_open_database(session) match {
-        case None => init(session, timeout = timeout)
+      def default: Session_Context = init(name, deps, ancestors, timeout = timeout)
+
+      store.try_open_database(name) match {
+        case None => default
         case Some(db) =>
           def ignore_error(msg: String) = {
             progress.echo_warning(
-              "Ignoring bad database " + db + " for session " + quote(session) +
+              "Ignoring bad database " + db + " for session " + quote(name) +
               if_proper(msg, ":\n" + msg))
-            init(session, timeout = timeout)
+            default
           }
           try {
-            val command_timings = store.read_command_timings(db, session)
+            val command_timings = store.read_command_timings(db, name)
             val elapsed =
-              store.read_session_timing(db, session) match {
+              store.read_session_timing(db, name) match {
                 case Markup.Elapsed(s) => Time.seconds(s)
                 case _ => Time.zero
               }
-            new Session_Context(session, timeout, elapsed, command_timings)
+            new Session_Context(
+              name, deps, ancestors, timeout, elapsed, command_timings)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -78,7 +86,9 @@
   }
 
   final class Session_Context(
-    val session: String,
+    val name: String,
+    val deps: List[String],
+    val ancestors: List[String],
     val timeout: Time,
     val old_time: Time,
     val old_command_timings_blob: Bytes
@@ -86,7 +96,7 @@
     def is_empty: Boolean =
       old_time.is_zero && old_command_timings_blob.is_empty
 
-    override def toString: String = session
+    override def toString: String = name
   }
 
   class Build_Session(

--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 14:22:15 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 14:47:20 2023 +0100
@@ -37,8 +37,13 @@
         Map.from(
           for (name <- build_graph.keys_iterator)
           yield {
-            val timeout = sessions_structure(name).timeout
-            name -> Build_Job.Session_Context.load(name, timeout, store, progress = progress)
+            val info = sessions_structure(name)
+            val ancestors =
+              sessions_structure.build_requirements(List(name)).filterNot(_ == name)
+            val session_context =
+              Build_Job.Session_Context.load(
+                name, info.deps, ancestors, info.timeout, store, progress = progress)
+            name -> session_context
           })
 
       val sessions_time = {
@@ -98,11 +103,12 @@
   ) {
     def sessions_structure: Sessions.Structure = deps.sessions_structure
 
-    def session_context(session: String): Build_Job.Session_Context =
-      sessions.getOrElse(session, Build_Job.Session_Context.init(session))
-
     def old_command_timings(session: String): List[Properties.T] =
-      Properties.uncompress(session_context(session).old_command_timings_blob, cache = store.cache)
+      sessions.get(session) match {
+        case Some(session_context) =>
+          Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache)
+        case None => Nil
+      }
 
     def do_store(session: String): Boolean =
       build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)