src/Pure/ML/ml_heap.scala

--- a/src/Pure/ML/ml_heap.scala	Mon Feb 19 16:04:00 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Mon Feb 19 16:25:06 2024 +0100
@@ -97,6 +97,14 @@
           sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))),
         List.from[Bytes], _.bytes(Slices.content))
 
+    def write_slice(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit =
+      db.execute_statement(Slices.table.insert(), body =
+      { stmt =>
+        stmt.string(1) = name
+        stmt.int(2) = slice
+        stmt.bytes(3) = content
+      })
+
     def clean_entry(db: SQL.Database, name: String): Unit = {
       for (table <- List(Base.table, Slices.table)) {
         db.execute_statement(table.delete(sql = Base.name.where_equal(name)))
@@ -104,7 +112,7 @@
       db.create_view(Slices_Size.table)
     }
 
-    def prepare_entry(db: SQL.Database, name: String): Unit =
+    def init_entry(db: SQL.Database, name: String): Unit =
       db.execute_statement(Base.table.insert(), body =
         { stmt =>
           stmt.string(1) = name
@@ -112,14 +120,6 @@
           stmt.string(3) = None
         })
 
-    def write_slice(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit =
-      db.execute_statement(Slices.table.insert(), body =
-      { stmt =>
-        stmt.string(1) = name
-        stmt.int(2) = slice
-        stmt.bytes(3) = content
-      })
-
     def finish_entry(db: SQL.Database, name: String, size: Long, digest: SHA1.Digest): Unit =
       db.execute_statement(
         Base.table.update(List(Base.size, Base.digest), sql = Base.name.where_equal(name)),
@@ -159,7 +159,7 @@
 
         try {
           private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
-            private_data.prepare_entry(db, session_name)
+            private_data.init_entry(db, session_name)
           }
 
           for (i <- 0 until slices) {