--- 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 =
--- 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)