# HG changeset patch
# User wenzelm
# Date 1676152971 -3600
# Node ID b810e99b5afba07f1c51876c1db6e59c6539a78a
# Parent  8d34f53871b475b90b18d6d08f791263d66daf2c
clarified static build_context vs. dynamic queue;

diff -r 8d34f53871b4 -r b810e99b5afb src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 22:59:23 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 23:02:51 2023 +0100
@@ -42,8 +42,6 @@
     build_graph: Graph[String, Sessions.Info],
     build_order: SortedSet[String]
   ) {
-    def is_inner(name: String): Boolean = !build_graph.is_maximal(name)
-
     def is_empty: Boolean = build_graph.is_empty
 
     def - (name: String): Queue =
@@ -177,8 +175,6 @@
     val build_context =
       Build_Process.Context(build_deps.sessions_structure, store, progress = progress)
 
-    val queue = Queue(build_context)
-
     store.prepare_output_dir()
 
     if (clean_build) {
@@ -302,7 +298,8 @@
                   else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
 
                 val do_store =
-                  build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
+                  build_heap || Sessions.is_pure(session_name) ||
+                  build_context.is_inner(session_name)
 
                 val (current, output_heap) = {
                   store.try_open_database(session_name) match {
@@ -374,7 +371,7 @@
           progress.echo_warning("Nothing to build")
           Map.empty[String, Result]
         }
-        else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
+        else Isabelle_Thread.uninterruptible { loop(Queue(build_context), Map.empty, Map.empty) }
 
       val sessions_ok: List[String] =
         (for {
diff -r 8d34f53871b4 -r b810e99b5afb src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 22:59:23 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 23:02:51 2023 +0100
@@ -121,5 +121,8 @@
   ) {
     def apply(session: String): Session_Context =
       sessions.getOrElse(session, Session_Context.empty(session, Time.zero))
+
+    def is_inner(session: String): Boolean =
+      !sessions_structure.build_graph.is_maximal(session)
   }
 }