diff -r 55a6aa77f3d8 -r 8a7df40375ae src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Jun 14 11:47:43 2023 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Jun 14 12:10:40 2023 +0200 @@ -1618,10 +1618,8 @@ val all_tables: SQL.Tables = SQL.Tables(Session_Info.table, Sources.table, Export.Data.table, Document_Build.Data.table) - def init_session_info(db: SQL.Database, name: String): Boolean = { - db.transaction { - all_tables.create_lock(db) - + def init_session_info(db: SQL.Database, name: String): Boolean = + db.transaction_lock(all_tables, create = true) { val already_defined = session_info_defined(db, name) db.execute_statement( @@ -1638,7 +1636,6 @@ already_defined } - } def session_info_exists(db: SQL.Database): Boolean = { val tables = db.tables