src/Pure/General/sql.scala
changeset 78551 d0c9d277620e
parent 78547 7f564f33172b
child 78554 54991440905e
--- a/src/Pure/General/sql.scala	Mon Aug 21 11:56:07 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Aug 21 12:34:53 2023 +0200
@@ -323,9 +323,9 @@
 
     def execute(): Boolean = rep.execute()
 
-    def execute_batch(batch: Statement => IterableOnce[Boolean]): Unit = {
+    def execute_batch(batch: IterableOnce[Statement => Boolean]): Unit = {
       var proper = false
-      for (ok <- batch(this).iterator if ok) { rep.addBatch(); proper = true }
+      for (body <- batch.iterator if body(this)) { rep.addBatch(); proper = true }
       if (proper) {
         val res = rep.executeBatch()
         if (!res.forall(i => i >= 0 || i == java.sql.Statement.SUCCESS_NO_INFO)) {
@@ -520,7 +520,7 @@
 
     def execute_batch_statement(
       sql: Source,
-      batch: Statement => IterableOnce[Boolean] = _ => Nil
+      batch: IterableOnce[Statement => Boolean] = Nil
     ): Unit = using_statement(sql) { stmt => stmt.execute_batch(batch) }
 
     def execute_query_statement[A, B](