# HG changeset patch
# User wenzelm
# Date 1709583742 -3600
# Node ID e9e74577755f32ee69590e225510abe38e42cbc8
# Parent  7e05515cadc07873b0ec615bd46f16476cbbc35b
tuned messages;

diff -r 7e05515cadc0 -r e9e74577755f src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Mon Mar 04 21:18:24 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Mon Mar 04 21:22:22 2024 +0100
@@ -231,7 +231,7 @@
 
         if (log_db0.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
 
-        private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
+        private_data.transaction_lock(db, create = true, label = "ML_Heap.store") {
           private_data.init_entry(db, session.name, heap_size0, heap_digest0, log_db0)
           for (content <- content0) private_data.write_slice(db, session.name, 0, content)
         }
@@ -241,20 +241,20 @@
       if (slices > 1) {
         for (i <- 1 until slices) {
           val content = slice_content(i)
-          private_data.transaction_lock(db, label = "ML_Heap.store2") {
+          private_data.transaction_lock(db, label = "ML_Heap.store" + i) {
             private_data.write_slice(db, session.name, i, content)
           }
         }
 
         if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
 
-        private_data.transaction_lock(db, label = "ML_Heap.store3") {
+        private_data.transaction_lock(db, label = "ML_Heap.store_update") {
           private_data.update_entry(db, session.name, heap_size, heap_digest, log_db)
         }
       }
     }
     catch { case exn: Throwable =>
-      private_data.transaction_lock(db, create = true, label = "ML_Heap.store4") {
+      private_data.transaction_lock(db, create = true, label = "ML_Heap.store_clean") {
         private_data.clean_entry(db, session.name)
       }
       throw exn