diff -r 70a65ee4a738 -r 72e77c8307ec src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Sat Aug 06 14:06:29 2022 +0200 +++ b/src/Pure/General/sql.scala Sat Aug 06 14:11:19 2022 +0200 @@ -303,13 +303,13 @@ def close(): Unit = connection.close() def transaction[A](body: => A): A = { - val auto_commit = connection.getAutoCommit + val auto_commit = connection.getAutoCommit() try { connection.setAutoCommit(false) - val savepoint = connection.setSavepoint + val savepoint = connection.setSavepoint() try { val result = body - connection.commit + connection.commit() result } catch { case exn: Throwable => connection.rollback(savepoint); throw exn } @@ -403,7 +403,7 @@ def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source = table.insert_cmd("INSERT OR IGNORE", sql = sql) - def rebuild: Unit = using_statement("VACUUM")(_.execute()) + def rebuild(): Unit = using_statement("VACUUM")(_.execute()) } }