# HG changeset patch
# User wenzelm
# Date 1687340531 -7200
# Node ID 721c118f7001e0efef35e93806498b718351c40a
# Parent  26b9b40ec1afbcff278b417d08eae94ed694ad3f
proper ML_Heap.clean_entry;

diff -r 26b9b40ec1af -r 721c118f7001 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Jun 21 11:15:04 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Wed Jun 21 11:42:11 2023 +0200
@@ -111,6 +111,9 @@
     val all_tables: SQL.Tables = SQL.Tables(Base.table, Slices.table)
   }
 
+  def clean_entry(db: SQL.Database, name: String): Unit =
+    db.transaction_lock(Data.all_tables, create = true) { Data.clean_entry(db, name) }
+
   def write_digest(
     database: Option[SQL.Database],
     heap: Path,
diff -r 26b9b40ec1af -r 721c118f7001 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Wed Jun 21 11:15:04 2023 +0200
+++ b/src/Pure/Thy/store.scala	Wed Jun 21 11:42:11 2023 +0200
@@ -312,7 +312,12 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    if (init) using(open_database(name, output = true))(init_session_info(_, name))
+    if (init) {
+      using(open_database(name, output = true)) { db =>
+        if (build_database_test && build_database_server) ML_Heap.clean_entry(db, name)
+        init_session_info(db, name)
+      }
+    }
 
     if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
   }