# 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 }) }