--- a/src/Pure/Tools/build.scala Sat Feb 11 23:02:51 2023 +0100
+++ b/src/Pure/Tools/build.scala Sat Feb 11 23:24:57 2023 +0100
@@ -297,10 +297,7 @@
}
else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
- val do_store =
- build_heap || Sessions.is_pure(session_name) ||
- build_context.is_inner(session_name)
-
+ val do_store = build_heap || build_context.build_heap(session_name)
val (current, output_heap) = {
store.try_open_database(session_name) match {
case Some(db) =>
--- a/src/Pure/Tools/build_process.scala Sat Feb 11 23:02:51 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sat Feb 11 23:24:57 2023 +0100
@@ -122,7 +122,7 @@
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)
+ def build_heap(session: String): Boolean =
+ Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)
}
}