src/Pure/Thy/store.scala
changeset 78227 1ba48d402005
parent 78223 2d2417a63314
child 78260 0a7f7abbe4f0
--- 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
   }