discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
--- 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") {
--- 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 }
}
--- 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