# HG changeset patch
# User wenzelm
# Date 1686737440 -7200
# Node ID 8a7df40375ae77684e193c14c7b7f59396e26e92
# Parent  55a6aa77f3d8f8126dcf9f1e593fe4d6858a7206
tuned signature: more operations;

diff -r 55a6aa77f3d8 -r 8a7df40375ae src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Jun 14 11:47:43 2023 +0200
+++ b/src/Pure/General/sql.scala	Wed Jun 14 12:10:40 2023 +0200
@@ -246,7 +246,8 @@
     }
 
     // requires transaction
-    def lock(db: Database): Unit = {
+    def lock(db: Database, create: Boolean = false): Unit = {
+      if (create) foreach(db.create_table(_))
       val sql = db.lock_tables(list)
       if (sql.nonEmpty) db.execute_statement(sql)
     }
@@ -409,8 +410,8 @@
       finally { connection.setAutoCommit(auto_commit) }
     }
 
-    def transaction_lock[A](tables: Tables)(body: => A): A =
-      transaction { tables.lock(db); body }
+    def transaction_lock[A](tables: Tables, create: Boolean = false)(body: => A): A =
+      transaction { tables.lock(db, create = create); body }
 
     def lock_tables(tables: List[Table]): Source = ""  // PostgreSQL only
 
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
diff -r 55a6aa77f3d8 -r 8a7df40375ae src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 14 11:47:43 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 14 12:10:40 2023 +0200
@@ -124,8 +124,7 @@
     def prepare_database(): Unit = {
       using_option(store.open_build_database()) { db =>
         val shared_db = db.is_postgresql
-        db.transaction {
-          Data.all_tables.create_lock(db)
+        db.transaction_lock(Data.all_tables, create = true) {
           Data.clean_build(db)
           if (shared_db) store.all_tables.create_lock(db)
         }