more thorough database checks;
authorwenzelm
Thu, 16 Mar 2023 15:38:32 +0100
changeset 77676 649708f75c6f
parent 77675 9e5f8f6e58a0
child 77677 daaaf59375e9
more thorough database checks;
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,