# HG changeset patch
# User wenzelm
# Date 1698759351 -3600
# Node ID f627ab8c276ca83297cfe8c60353a2201293fd0a
# Parent  cc8391b92747436a09ad4f923f429de7b67b0c05
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;

diff -r cc8391b92747 -r f627ab8c276c src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Oct 31 14:26:19 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 31 14:35:51 2023 +0100
@@ -846,8 +846,7 @@
         port = options.int("build_log_database_port"),
         ssh_host = options.string("build_log_ssh_host"),
         ssh_port = options.int("build_log_ssh_port"),
-        ssh_user = options.string("build_log_ssh_user"),
-        synchronous_commit = options.string("build_log_database_synchronous_commit"))
+        ssh_user = options.string("build_log_ssh_user"))
 
     def init_database(db: SQL.Database, minimal: Boolean = false): Unit =
       private_data.transaction_lock(db, create = true, label = "build_log_init") {
diff -r cc8391b92747 -r f627ab8c276c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Oct 31 14:26:19 2023 +0100
+++ b/src/Pure/General/sql.scala	Tue Oct 31 14:35:51 2023 +0100
@@ -663,8 +663,7 @@
     password: String,
     database: String = "",
     server: SSH.Server = default_server,
-    server_close: Boolean = false,
-    synchronous_commit: String = "off"
+    server_close: Boolean = false
   ): Database = {
     init_jdbc
 
@@ -680,16 +679,7 @@
         if_proper(ssh, " via ssh " + quote(ssh.get.toString))
 
     val connection = DriverManager.getConnection(url, user, password)
-    val db = new Database(connection, print, server, server_close)
-
-    try {
-      if (synchronous_commit.nonEmpty) {
-        db.execute_statement("SET synchronous_commit = " + SQL.string(synchronous_commit))
-      }
-    }
-    catch { case exn: Throwable => db.close(); throw exn }
-
-    db
+    new Database(connection, print, server, server_close)
   }
 
   def open_server(
@@ -720,8 +710,7 @@
     port: Int = 0,
     ssh_host: String = "",
     ssh_port: Int = 0,
-    ssh_user: String = "",
-    synchronous_commit: String = ""
+    ssh_user: String = ""
   ): PostgreSQL.Database = {
     val db_server =
       if (server.defined) server
@@ -732,7 +721,7 @@
     val server_close = !server.defined
     try {
       open_database(user = user, password = password, database = database,
-        server = db_server, server_close = server_close, synchronous_commit = synchronous_commit)
+        server = db_server, server_close = server_close)
     }
     catch { case exn: Throwable if server_close => db_server.close(); throw exn }
   }
diff -r cc8391b92747 -r f627ab8c276c src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Tue Oct 31 14:26:19 2023 +0100
+++ b/src/Pure/Thy/store.scala	Tue Oct 31 14:35:51 2023 +0100
@@ -316,8 +316,7 @@
       port = options.int("build_database_port"),
       ssh_host = options.string("build_database_ssh_host"),
       ssh_port = options.int("build_database_ssh_port"),
-      ssh_user = options.string("build_database_ssh_user"),
-      synchronous_commit = options.string("build_database_synchronous_commit"))
+      ssh_user = options.string("build_database_ssh_user"))
 
   def maybe_open_database_server(server: SSH.Server = SSH.no_server): Option[SQL.Database] =
     if (build_database_server) Some(open_database_server(server = server)) else None