--- a/src/Pure/Thy/store.scala Wed Jun 28 12:39:43 2023 +0200
+++ b/src/Pure/Thy/store.scala Wed Jun 28 13:30:53 2023 +0200
@@ -313,9 +313,7 @@
case Some(db) =>
ML_Heap.clean_entry(db, name)
clean_session_info(db, name)
- case None =>
- if (session_init) using(open_database(name, output = true))(clean_session_info(_, name))
- false
+ case None => false
}
val del =
@@ -326,6 +324,10 @@
path = dir + file if path.is_file
} yield path.file.delete
+ if (database_server.isEmpty && session_init) {
+ using(open_database(name, output = true))(clean_session_info(_, name))
+ }
+
if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
}