# HG changeset patch
# User wenzelm
# Date 1687278197 -7200
# Node ID 31835adf148ae8be0d9e0a4317bbdbe2086a0d1a
# Parent  c2fbe48e9df422bf70203dfe4881cd887e8fda4d
tuned signature;

diff -r c2fbe48e9df4 -r 31835adf148a src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Tue Jun 20 16:48:47 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Tue Jun 20 18:23:17 2023 +0200
@@ -17,7 +17,7 @@
 
   private val sha1_prefix = "SHA1:"
 
-  def read_digest(heap: Path): Option[SHA1.Digest] = {
+  def read_file_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
       val l = sha1_prefix.length
       val m = l + SHA1.digest_length
@@ -33,8 +33,8 @@
     else None
   }
 
-  def write_digest(heap: Path): SHA1.Digest =
-    read_digest(heap) getOrElse {
+  def write_file_digest(heap: Path): SHA1.Digest =
+    read_file_digest(heap) getOrElse {
       val digest = SHA1.digest(heap)
       File.append(heap, sha1_prefix + digest.toString)
       digest
diff -r c2fbe48e9df4 -r 31835adf148a src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Tue Jun 20 16:48:47 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 20 18:23:17 2023 +0200
@@ -230,7 +230,7 @@
   def find_heap_shasum(name: String): SHA1.Shasum =
     (for {
       path <- find_heap(name)
-      digest <- ML_Heap.read_digest(path)
+      digest <- ML_Heap.read_file_digest(path)
     } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
 
   def the_heap(name: String): Path =
diff -r c2fbe48e9df4 -r 31835adf148a src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Jun 20 16:48:47 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue Jun 20 18:23:17 2023 +0200
@@ -451,7 +451,7 @@
 
         val output_shasum =
           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)
+            SHA1.shasum(ML_Heap.write_file_digest(store.output_heap(session_name)), session_name)
           }
           else SHA1.no_shasum