# HG changeset patch
# User wenzelm
# Date 1676154297 -3600
# Node ID 25e923c57af7ce9448229c9272c5223a37cc3626
# Parent  b810e99b5afba07f1c51876c1db6e59c6539a78a
clarified signature;

diff -r b810e99b5afb -r 25e923c57af7 src/Pure/Tools/build.scala
--- 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) =>
diff -r b810e99b5afb -r 25e923c57af7 src/Pure/Tools/build_process.scala
--- 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)
   }
 }