# HG changeset patch
# User wenzelm
# Date 1713259230 -7200
# Node ID 4b95a1d8b2c9b93e0ad4213060498a98240c747d
# Parent  c729b1d589820eb1447712c43ac5330a97ef6c53
tuned;

diff -r c729b1d58982 -r 4b95a1d8b2c9 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Tue Apr 16 11:00:46 2024 +0200
+++ b/src/Pure/ML/ml_heap.scala	Tue Apr 16 11:20:30 2024 +0200
@@ -11,16 +11,14 @@
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
+  private val sha1_length = sha1_prefix.length + SHA1.digest_length
 
   def read_file_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
-      val l = sha1_prefix.length
-      val m = l + SHA1.digest_length
-      val n = File.size(heap)
-      val bs = Bytes.read_file(heap, offset = n - m)
-      if (bs.length == m) {
+      val bs = Bytes.read_file(heap, offset = File.size(heap) - sha1_length)
+      if (bs.length == sha1_length) {
         val s = bs.text
-        if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
+        if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(sha1_prefix.length)))
         else None
       }
       else None
@@ -204,7 +202,7 @@
     val heap_digest = session.heap.map(write_file_digest)
     val heap_size =
       session.heap match {
-        case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length
+        case Some(heap) => File.size(heap) - sha1_length
         case None => 0L
       }