# HG changeset patch
# User wenzelm
# Date 1692623062 -7200
# Node ID 54991440905e2e7f5f5e582e36c906f619bc094b
# Parent  66fc98b4557ba8c6a2166497ecc9c73f36250ed3
clarified signature: proper treatment of implicit state (amending d0c9d277620e);

diff -r 66fc98b4557b -r 54991440905e src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Aug 21 13:01:45 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Aug 21 15:04:22 2023 +0200
@@ -323,10 +323,10 @@
 
     def execute(): Boolean = rep.execute()
 
-    def execute_batch(batch: IterableOnce[Statement => Boolean]): Unit = {
-      var proper = false
-      for (body <- batch.iterator if body(this)) { rep.addBatch(); proper = true }
-      if (proper) {
+    def execute_batch(batch: IterableOnce[Statement => Unit]): Unit = {
+      val it = batch.iterator
+      if (it.nonEmpty) {
+        for (body <- it) { body(this); rep.addBatch() }
         val res = rep.executeBatch()
         if (!res.forall(i => i >= 0 || i == java.sql.Statement.SUCCESS_NO_INFO)) {
           throw new Batch_Error(res.toList)
@@ -520,7 +520,7 @@
 
     def execute_batch_statement(
       sql: Source,
-      batch: IterableOnce[Statement => Boolean] = Nil
+      batch: IterableOnce[Statement => Unit] = Nil
     ): Unit = using_statement(sql) { stmt => stmt.execute_batch(batch) }
 
     def execute_query_statement[A, B](
diff -r 66fc98b4557b -r 54991440905e src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon Aug 21 13:01:45 2023 +0200
+++ b/src/Pure/System/progress.scala	Mon Aug 21 15:04:22 2023 +0200
@@ -176,7 +176,6 @@
           stmt.int(3) = message.kind.id
           stmt.string(4) = message.text
           stmt.bool(5) = message.verbose
-          true
         })
     }
   }
diff -r 66fc98b4557b -r 54991440905e src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Aug 21 13:01:45 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Aug 21 15:04:22 2023 +0200
@@ -94,22 +94,17 @@
         }
       )
 
-    def write_entries(db: SQL.Database, entries: List[Option[Entry]]): Unit =
+    def write_entries(db: SQL.Database, entries: List[Entry]): Unit =
       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
-            stmt.string(3) = entry.name
-            stmt.bool(4) = entry.executable
-            stmt.bool(5) = compressed
-            stmt.bytes(6) = bs
-            true
-          }
+        for (entry <- entries) yield { (stmt: SQL.Statement) =>
+          val (compressed, bs) = entry.body.join
+          stmt.string(1) = entry.session_name
+          stmt.string(2) = entry.theory_name
+          stmt.string(3) = entry.name
+          stmt.bool(4) = entry.executable
+          stmt.bool(5) = compressed
+          stmt.bytes(6) = bs
         })
-      )
 
     def read_theory_names(db: SQL.Database, session_name: String): List[String] =
       db.execute_query_statement(
@@ -288,7 +283,7 @@
 
                   val entries = buffer.toList
                   try {
-                    private_data.write_entries(db, entries)
+                    private_data.write_entries(db, entries.flatten)
                     val ok = Exn.Res[Unit](())
                     entries.map(_ => ok)
                   }
diff -r 66fc98b4557b -r 54991440905e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Aug 21 13:01:45 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Mon Aug 21 15:04:22 2023 +0200
@@ -459,7 +459,6 @@
             stmt.long(7) = session.old_time.ms
             stmt.bytes(8) = session.old_command_timings_blob
             stmt.string(9) = session.build_uuid
-            true
           })
       }
 
@@ -602,7 +601,6 @@
             stmt.string(2) = cat_lines(task.deps)
             stmt.string(3) = JSON.Format(task.info)
             stmt.string(4) = task.build_uuid
-            true
           })
       }
 
@@ -659,7 +657,6 @@
             stmt.string(3) = job.build_uuid
             stmt.string(4) = job.node_info.hostname
             stmt.int(5) = job.node_info.numa_node
-            true
           })
       }
 
@@ -755,7 +752,6 @@
             stmt.long(11) = process_result.timing.gc.ms
             stmt.string(12) = result.output_shasum.toString
             stmt.bool(13) = result.current
-            true
           })
       }