# HG changeset patch
# User wenzelm
# Date 1678977512 -3600
# Node ID 649708f75c6f545a809d851247545609524e4fc5
# Parent  9e5f8f6e58a0100cee5914c9003ef98272fe497e
more thorough database checks;

diff -r 9e5f8f6e58a0 -r 649708f75c6f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 16 15:16:17 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 15:38:32 2023 +0100
@@ -1620,9 +1620,9 @@
 
     def init_session_info(db: SQL.Database, name: String): Boolean = {
       db.transaction {
-        val already_defined = session_info_defined(db, name)
+        all_tables.create_lock(db)
 
-        all_tables.create_lock(db)
+        val already_defined = session_info_defined(db, name)
 
         db.execute_statement(
           Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))
@@ -1642,15 +1642,13 @@
 
     def session_info_exists(db: SQL.Database): Boolean = {
       val tables = db.tables
-      tables.contains(Session_Info.table.name) &&
-      tables.contains(Export.Data.table.name)
+      all_tables.forall(table => tables.contains(table.name))
     }
 
     def session_info_defined(db: SQL.Database, name: String): Boolean =
-      session_info_exists(db) &&
-        db.execute_query_statementB(
-          Session_Info.table.select(List(Session_Info.session_name),
-            sql = Session_Info.session_name.where_equal(name)))
+      db.execute_query_statementB(
+        Session_Info.table.select(List(Session_Info.session_name),
+          sql = Session_Info.session_name.where_equal(name)))
 
     def write_session_info(
       db: SQL.Database,