# HG changeset patch
# User wenzelm
# Date 1692614093 -7200
# Node ID d0c9d277620e6cfda9dff2ea40207845cc779650
# Parent  d8cc0f625b5229369da009509a8965d98b638f20
clarified signature: more robust treatment of implicit state;

diff -r d8cc0f625b52 -r d0c9d277620e src/Pure/General/sql.scala
--- 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](
diff -r d8cc0f625b52 -r d0c9d277620e src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon Aug 21 11:56:07 2023 +0200
+++ b/src/Pure/System/progress.scala	Mon Aug 21 12:34:53 2023 +0200
@@ -169,16 +169,15 @@
       context: Long,
       messages: List[(Long, Message)]
     ): Unit = {
-      db.execute_batch_statement(Messages.table.insert(), batch = { stmt =>
-        for ((serial, message) <- messages.iterator) yield {
+      db.execute_batch_statement(Messages.table.insert(), batch =
+        for ((serial, message) <- messages) yield { (stmt: SQL.Statement) =>
           stmt.long(1) = context
           stmt.long(2) = serial
           stmt.int(3) = message.kind.id
           stmt.string(4) = message.text
           stmt.bool(5) = message.verbose
           true
-        }
-      })
+        })
     }
   }
 }
diff -r d8cc0f625b52 -r d0c9d277620e src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Aug 21 11:56:07 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Aug 21 12:34:53 2023 +0200
@@ -95,10 +95,10 @@
       )
 
     def write_entries(db: SQL.Database, entries: List[Option[Entry]]): Unit =
-      db.execute_batch_statement(Base.table.insert(), batch = { stmt =>
-        entries.iterator.map({
-          case None => false
-          case Some(entry) =>
+      db.execute_batch_statement(Base.table.insert(), batch =
+        entries.map({
+          case None => _ => false
+          case Some(entry) => { (stmt: SQL.Statement) =>
             val (compressed, bs) = entry.body.join
             stmt.string(1) = entry.session_name
             stmt.string(2) = entry.theory_name
@@ -107,8 +107,9 @@
             stmt.bool(5) = compressed
             stmt.bytes(6) = bs
             true
+          }
         })
-      })
+      )
 
     def read_theory_names(db: SQL.Database, session_name: String): List[String] =
       db.execute_query_statement(