# HG changeset patch
# User wenzelm
# Date 1713273073 -7200
# Node ID 0323cd9fcab977cb5033b58d77f28a4032ac5fd2
# Parent  61b8f6ac6860908a820090338df07c3fc42c3950
clarified signature;

diff -r 61b8f6ac6860 -r 0323cd9fcab9 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build.scala	Tue Apr 16 15:11:13 2024 +0200
@@ -36,7 +36,7 @@
     numa_shuffling: Boolean = false,
     numa_nodes: List[Int] = Nil,
     clean_sessions: List[String] = Nil,
-    build_heap: Boolean = false,
+    store_heap: Boolean = false,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
@@ -256,7 +256,7 @@
       val build_context =
         Context(store, build_deps, engine = engine, afp_root = afp_root,
           build_hosts = build_hosts, hostname = hostname(build_options),
-          clean_sessions = clean_sessions, build_heap = build_heap,
+          clean_sessions = clean_sessions, store_heap = build_heap,
           numa_shuffling = numa_shuffling, numa_nodes = numa_nodes,
           fresh_build = fresh_build, no_build = no_build, session_setup = session_setup,
           jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true)
diff -r 61b8f6ac6860 -r 0323cd9fcab9 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Tue Apr 16 15:11:13 2024 +0200
@@ -94,6 +94,9 @@
     def iterator: Iterator[Build_Job.Session_Context] =
       for (name <- graph.topological_order.iterator) yield apply(name)
 
+    def store_heap(name: String): Boolean =
+      isabelle.Sessions.is_pure(name) || iterator.exists(_.ancestors.contains(name))
+
     def data: Library.Update.Data[Build_Job.Session_Context] =
       Map.from(for ((_, (session, _)) <- graph.iterator) yield session.name -> session)
 
@@ -1165,9 +1168,7 @@
       if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
       else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
 
-    val store_heap =
-      build_context.build_heap || Sessions.is_pure(session_name) ||
-      state.sessions.iterator.exists(_.ancestors.contains(session_name))
+    val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
 
     val (current, output_shasum) =
       store.check_output(_database_server, session_name,
diff -r 61b8f6ac6860 -r 0323cd9fcab9 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Tue Apr 16 15:11:13 2024 +0200
@@ -1124,9 +1124,7 @@
             if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
             else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
 
-          val store_heap =
-            build_context.build_heap || Sessions.is_pure(session_name) ||
-              state.sessions.iterator.exists(_.ancestors.contains(session_name))
+          val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
 
           store.check_output(
             _database_server, session_name,