# HG changeset patch
# User wenzelm
# Date 1708543290 -3600
# Node ID 45af93b0370ad49c9bfa2ccbe34b376083923cd9
# Parent  0554a32a6ef4ff37d98cbeebc1678267458dcf8d
tuned signature;
tuned messages;

diff -r 0554a32a6ef4 -r 45af93b0370a src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Wed Feb 21 19:59:35 2024 +0100
+++ b/src/Pure/Build/store.scala	Wed Feb 21 20:21:30 2024 +0100
@@ -34,6 +34,8 @@
     val log_db: Option[Path],
     dirs: List[Path]
   ) {
+    def log_db_name: String = Store.log_db(name).implode
+
     def defined: Boolean = heap.isDefined || log_db.isDefined
 
     def the_heap: Path =
diff -r 0554a32a6ef4 -r 45af93b0370a src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Feb 21 19:59:35 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Wed Feb 21 20:21:30 2024 +0100
@@ -219,7 +219,7 @@
           uuid <- proper_string(Store.read_build_uuid(path, session.name))
         } yield Log_DB(uuid, Bytes.read(path))
 
-      if (opt_log_db.isDefined) progress.echo("Storing " + session.name + ".db ...")
+      if (opt_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, opt_digest, opt_log_db)
@@ -279,7 +279,7 @@
             val file_uuid = Store.read_build_uuid(path, session.name)
             private_data.read_log_db(db, session.name, old_uuid = file_uuid) match {
               case Some(log_db) if file_uuid.isEmpty =>
-                progress.echo("Restoring " + session.name + ".db ...")
+                progress.echo("Restoring " + session.log_db_name + " ...")
                 Isabelle_System.make_directory(path.expand.dir)
                 Bytes.write(path, log_db.content)
               case Some(_) => error("Incoherent content for session database " + path)