# HG changeset patch
# User wenzelm
# Date 1708783850 -3600
# Node ID 8544f10451231a9c669e089ee04f0be53f497501
# Parent  fba02e281b4465b2874345e73cfb9daceca626b5
tuned;

diff -r fba02e281b44 -r 8544f1045123 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sat Feb 24 11:27:04 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sat Feb 24 15:10:50 2024 +0100
@@ -204,6 +204,15 @@
 
     val slice_size = slice.bytes max Space.MiB(1).bytes
     val slices = (heap_size.toDouble / slice_size.toDouble).ceil.toInt
+    val step = if (slices == 0) 0L else (heap_size.toDouble / slices.toDouble).ceil.toLong
+
+    def slice_content(i: Int): Bytes = {
+      val j = i + 1
+      val offset = step * i
+      val limit = if (j < slices) step * j else heap_size
+      Bytes.read_file(session.the_heap, offset = offset, limit = limit)
+        .compress(cache = cache)
+    }
 
     try {
       if (slices == 0 && log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
@@ -214,14 +223,8 @@
 
       if (slices > 0) {
         progress.echo("Storing " + session.name + " ...")
-        val step = (heap_size.toDouble / slices.toDouble).ceil.toLong
         for (i <- 0 until slices) {
-          val j = i + 1
-          val offset = step * i
-          val limit = if (j < slices) step * j else heap_size
-          val content =
-            Bytes.read_file(session.the_heap, offset = offset, limit = limit)
-              .compress(cache = cache)
+          val content = slice_content(i)
           private_data.transaction_lock(db, label = "ML_Heap.store2") {
             private_data.write_slice(db, session.name, i, content)
           }