clarified static build_context vs. dynamic queue;
--- 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 {
--- 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)
}
}