# HG changeset patch
# User wenzelm
# Date 1677701279 -3600
# Node ID 4e8bec105ce5a1b5070f1394ef2947e17d31c770
# Parent  b474d39ddfeefb8e2522cb22838f98e1c1e745b3
tuned signature;

diff -r b474d39ddfee -r 4e8bec105ce5 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 21:04:28 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 21:07:59 2023 +0100
@@ -97,7 +97,7 @@
     build_context: Build_Process.Context,
     session_background: Sessions.Background,
     session_heaps: List[Path],
-    do_store: Boolean,
+    store_heap: Boolean,
     resources: Resources,
     input_shasum: SHA1.Shasum,
     override val node_info: Node_Info
@@ -124,7 +124,7 @@
         val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
 
         val eval_store =
-          if (do_store) {
+          if (store_heap) {
             (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
             List("ML_Heap.save_child " +
               ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
@@ -444,7 +444,7 @@
       }
 
       val output_shasum =
-        if (process_result.ok && do_store && store.output_heap(session_name).is_file) {
+        if (process_result.ok && store_heap && store.output_heap(session_name).is_file) {
           SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
         }
         else SHA1.no_shasum
diff -r b474d39ddfee -r 4e8bec105ce5 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 21:04:28 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 21:07:59 2023 +0100
@@ -112,7 +112,7 @@
         case None => Nil
       }
 
-    def do_store(name: String): Boolean =
+    def store_heap(name: String): Boolean =
       build_heap || Sessions.is_pure(name) ||
       sessions.valuesIterator.exists(_.ancestors.contains(name))
   }
@@ -561,7 +561,7 @@
       }
       else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
 
-    val do_store = build_context.do_store(session_name)
+    val store_heap = build_context.store_heap(session_name)
     val (current, output_shasum) = {
       store.try_open_database(session_name) match {
         case Some(db) =>
@@ -574,7 +574,7 @@
                 build.sources == build_context.sources_shasum(session_name) &&
                 build.input_heaps == input_shasum &&
                 build.output_heap == output_shasum &&
-                !(do_store && output_shasum.is_empty)
+                !(store_heap && output_shasum.is_empty)
               (current, output_shasum)
             case None => (false, SHA1.no_shasum)
           }
@@ -607,7 +607,7 @@
       }
     }
     else {
-      progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
+      progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...")
 
       store.clean_output(session_name)
       using(store.open_database(session_name, output = true))(
@@ -630,7 +630,7 @@
           val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
           val job =
             new Build_Job.Session_Job(build_context, session_background, session_heaps,
-              do_store, resources, input_shasum, node_info)
+              store_heap, resources, input_shasum, node_info)
           _state = state1.add_running(session_name, job)
           job
         }