src/Pure/Thy/store.scala

--- a/src/Pure/Thy/store.scala	Tue Jun 27 10:05:33 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 27 10:24:32 2023 +0200
@@ -304,10 +304,16 @@
 
   def prepare_output(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
 
-  def clean_output(name: String, init: Boolean = false): Option[Boolean] = {
+  def clean_output(
+    database_server: Option[SQL.Database],
+    name: String,
+    init: Boolean = false
+  ): Option[Boolean] = {
     val relevant_db =
-      build_database_server &&
-        using_option(try_open_database(name))(clean_session_info(_, name)).getOrElse(false)
+      database_server match {
+        case Some(db) => clean_session_info(db, name)
+        case None => false
+      }
 
     val del =
       for {
@@ -317,9 +323,7 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    using_optional(maybe_open_database_server()) { database =>
-      database.foreach(ML_Heap.clean_entry(_, name))
-    }
+    database_server.foreach(ML_Heap.clean_entry(_, name))
 
     if (init) {
       using(open_database(name, output = true))(clean_session_info(_, name))
@@ -384,7 +388,7 @@
         sql = Store.Data.Session_Info.session_name.where_equal(name)))
 
   def clean_session_info(db: SQL.Database, name: String): Boolean =
-    Store.Data.transaction_lock(db, create = true) {
+    Store.Data.transaction_lock(db, create = true, synchronized = true) {
       val already_defined = session_info_defined(db, name)
 
       db.execute_statement(
@@ -411,7 +415,7 @@
     build_log: Build_Log.Session_Info,
     build: Store.Build_Info
   ): Unit = {
-    Store.Data.transaction_lock(db) {
+    Store.Data.transaction_lock(db, synchronized = true) {
       Store.Data.write_sources(db, session_name, sources)
       Store.Data.write_session_info(db, cache.compress, session_name, build_log, build)
     }