# HG changeset patch
# User wenzelm
# Date 1708604376 -3600
# Node ID eb742d4e4dc9dd822a12a47940fe56191f64d5f3
# Parent  ab7ec4a29b9c1a6f228e80737b8208c02319c37d
minor performance tuning: just one transaction for log_db without heap;

diff -r ab7ec4a29b9c -r eb742d4e4dc9 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:12:10 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:19:36 2024 +0100
@@ -133,7 +133,7 @@
       }
     }
 
-    def init_entry(db: SQL.Database, name: String): Unit = {
+    def init_entry(db: SQL.Database, name: String, log_db: Option[Log_DB] = None): Unit = {
       clean_entry(db, name)
       for (table <- List(Size.table, Slices_Size.table)) {
         db.create_view(table)
@@ -143,8 +143,8 @@
           stmt.string(1) = name
           stmt.long(2) = None
           stmt.string(3) = None
-          stmt.string(4) = None
-          stmt.bytes(5) = None
+          stmt.string(4) = log_db.map(_.uuid)
+          stmt.bytes(5) = log_db.map(_.content)
         })
     }
 
@@ -210,27 +210,31 @@
       } yield Log_DB(uuid, Bytes.read(path))
 
     try {
+      if (slices == 0 && log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
+
       private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
-        private_data.init_entry(db, session.name)
+        private_data.init_entry(db, session.name, log_db = if (slices == 0) log_db else None)
       }
 
-      if (slices > 0) progress.echo("Storing " + session.name + " ...")
-      for (i <- 0 until slices) {
-        val j = i + 1
-        val offset = step * i
-        val limit = if (j < slices) step * j else size
-        val content =
-          Bytes.read_file(session.the_heap, offset = offset, limit = limit)
-            .compress(cache = cache)
-        private_data.transaction_lock(db, label = "ML_Heap.store2") {
-          private_data.write_slice(db, session.name, i, content)
+      if (slices > 0) {
+        progress.echo("Storing " + session.name + " ...")
+        for (i <- 0 until slices) {
+          val j = i + 1
+          val offset = step * i
+          val limit = if (j < slices) step * j else size
+          val content =
+            Bytes.read_file(session.the_heap, offset = offset, limit = limit)
+              .compress(cache = cache)
+          private_data.transaction_lock(db, label = "ML_Heap.store2") {
+            private_data.write_slice(db, session.name, i, content)
+          }
         }
-      }
+
+        if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
 
-      if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
-
-      private_data.transaction_lock(db, label = "ML_Heap.store3") {
-        private_data.finish_entry(db, session.name, size, heap_digest, log_db)
+        private_data.transaction_lock(db, label = "ML_Heap.store3") {
+          private_data.finish_entry(db, session.name, size, heap_digest, log_db)
+        }
       }
     }
     catch { case exn: Throwable =>