# HG changeset patch
# User wenzelm
# Date 1676152763 -3600
# Node ID 8d34f53871b475b90b18d6d08f791263d66daf2c
# Parent  792dad9cb04f6a92826f5e5b369852263205833f
clarified signature: make dynamic Queue from static Context;

diff -r 792dad9cb04f -r 8d34f53871b4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 22:36:13 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 22:59:23 2023 +0100
@@ -31,32 +31,23 @@
   /* queue with scheduling information */
 
   private object Queue {
-    def apply(
-      sessions_structure: Sessions.Structure,
-      store: Sessions.Store,
-      progress: Progress = new Progress
-    ): Queue = {
-      val build_context = Build_Process.Context(sessions_structure, store, progress = progress)
-      val build_graph = sessions_structure.build_graph
+    def apply(build_context: Build_Process.Context): Queue = {
+      val build_graph = build_context.sessions_structure.build_graph
       val build_order = SortedSet.from(build_graph.keys)(build_context.ordering)
-      new Queue(build_context, build_graph, build_order)
+      new Queue(build_graph, build_order)
     }
   }
 
   private class Queue(
-    build_context: Build_Process.Context,
     build_graph: Graph[String, Sessions.Info],
     build_order: SortedSet[String]
   ) {
-    def old_command_timings(name: String): List[Properties.T] =
-      build_context(name).old_command_timings
-
     def is_inner(name: String): Boolean = !build_graph.is_maximal(name)
 
     def is_empty: Boolean = build_graph.is_empty
 
     def - (name: String): Queue =
-      new Queue(build_context, build_graph.del_node(name), build_order - name)
+      new Queue(build_graph.del_node(name), build_order - name)
 
     def dequeue(skip: String => Boolean): Option[String] =
       build_order.iterator.dropWhile(name => skip(name) || !build_graph.is_minimal(name))
@@ -183,7 +174,10 @@
 
     /* main build process */
 
-    val queue = Queue(build_deps.sessions_structure, store, progress = progress)
+    val build_context =
+      Build_Process.Context(build_deps.sessions_structure, store, progress = progress)
+
+    val queue = Queue(build_context)
 
     store.prepare_output_dir()
 
@@ -350,7 +344,7 @@
                   val session_background = build_deps.background(session_name)
                   val resources =
                     new Resources(session_background, log = log,
-                      command_timings = queue.old_command_timings(session_name))
+                      command_timings = build_context(session_name).old_command_timings)
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
diff -r 792dad9cb04f -r 8d34f53871b4 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 22:36:13 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 22:59:23 2023 +0100
@@ -110,11 +110,12 @@
             }
         }
 
-      new Context(sessions, ordering)
+      new Context(sessions_structure, sessions, ordering)
     }
   }
 
   final class Context private(
+    val sessions_structure: Sessions.Structure,
     sessions: Map[String, Session_Context],
     val ordering: Ordering[String]
   ) {