tuned;

--- a/src/Pure/ML/ml_heap.scala	Sun Jan 15 20:20:59 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sun Jan 15 20:38:27 2023 +0100
@@ -48,11 +48,9 @@
   }
 
   def write_digest(heap: Path): String =
-    read_digest(heap) match {
-      case None =>
-        val s = SHA1.digest(heap).toString
-        File.append(heap, sha1_prefix + s)
-        s
-      case Some(s) => s
+    read_digest(heap) getOrElse {
+      val s = SHA1.digest(heap).toString
+      File.append(heap, sha1_prefix + s)
+      s
     }
 }

--- a/src/Pure/Tools/build_job.scala	Sun Jan 15 20:20:59 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sun Jan 15 20:38:27 2023 +0100
@@ -591,8 +591,9 @@
       else result1
 
     val heap_digest =
-      if (result2.ok && do_store && store.output_heap(session_name).is_file)
+      if (result2.ok && do_store && store.output_heap(session_name).is_file) {
         Some(ML_Heap.write_digest(store.output_heap(session_name)))
+      }
       else None
 
     (result2, heap_digest)