--- a/src/Pure/Thy/store.scala Tue Jun 27 14:50:48 2023 +0200
+++ b/src/Pure/Thy/store.scala Tue Jun 27 15:10:47 2023 +0200
@@ -305,12 +305,16 @@
def clean_output(
database_server: Option[SQL.Database],
name: String,
- init: Boolean = false
+ session_init: Boolean = false
): Option[Boolean] = {
val relevant_db =
database_server match {
- case Some(db) => clean_session_info(db, name)
- case None => false
+ 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
}
val del =
@@ -321,12 +325,6 @@
path = dir + file if path.is_file
} yield path.file.delete
- database_server.foreach(ML_Heap.clean_entry(_, name))
-
- if (init) {
- using(open_database(name, output = true))(clean_session_info(_, name))
- }
-
if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
}