# HG changeset patch
# User wenzelm
# Date 1678360381 -3600
# Node ID 308f3f48c2c70afcc9a223634d9704c7f2fd019d
# Parent  dd8b08729458cdc96b7ab2de350c98cbc74458ac
more robust transactions;

diff -r dd8b08729458 -r 308f3f48c2c7 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 09 11:55:20 2023 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 09 12:13:01 2023 +0100
@@ -370,6 +370,8 @@
     val port = SQL.Column.int("port")
     val password = SQL.Column.string("password")
     val table = SQL.Table("isabelle_servers", List(name, port, password))
+
+    val tables = SQL.Tables(table)
   }
 
   def list(db: SQLite.Database): List[Info] =
@@ -398,11 +400,11 @@
     using(SQLite.open_database(Data.database)) { db =>
       db.transaction {
         Isabelle_System.chmod("600", Data.database)
-        db.create_table(Data.table)
+        Data.tables.create_lock(db)
         list(db).filterNot(_.active).foreach(server_info =>
           db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))
       }
-      db.transaction {
+      db.transaction_lock(Data.tables) {
         find(db, name) match {
           case Some(server_info) => (server_info, None)
           case None =>
@@ -428,7 +430,7 @@
 
   def exit(name: String = default_name): Boolean = {
     using(SQLite.open_database(Data.database))(db =>
-      db.transaction {
+      db.transaction_lock(Data.tables) {
         find(db, name) match {
           case Some(server_info) =>
             using(server_info.connection())(_.write_line_message("shutdown"))