# HG changeset patch
# User wenzelm
# Date 1708603930 -3600
# Node ID ab7ec4a29b9c1a6f228e80737b8208c02319c37d
# Parent  909031707ff49d54741e6ab50558ba87b83a15cd
tuned;

diff -r 909031707ff4 -r ab7ec4a29b9c src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:00:58 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:12:10 2024 +0100
@@ -197,6 +197,18 @@
     val slices = (size.toDouble / slice_size.toDouble).ceil.toInt
     val step = if (slices > 0) (size.toDouble / slices.toDouble).ceil.toLong else 0L
 
+    val heap_digest =
+      for {
+        path <- session.heap
+        digest <- read_file_digest(path)
+      } yield digest
+
+    val log_db =
+      for {
+        path <- session.log_db
+        uuid <- proper_string(Store.read_build_uuid(path, session.name))
+      } yield Log_DB(uuid, Bytes.read(path))
+
     try {
       private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
         private_data.init_entry(db, session.name)
@@ -215,18 +227,6 @@
         }
       }
 
-      val heap_digest =
-        for {
-          path <- session.heap
-          digest <- read_file_digest(path)
-        } yield digest
-
-      val log_db =
-        for {
-          path <- session.log_db
-          uuid <- proper_string(Store.read_build_uuid(path, session.name))
-        } yield Log_DB(uuid, Bytes.read(path))
-
       if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
 
       private_data.transaction_lock(db, label = "ML_Heap.store3") {