# HG changeset patch
# User wenzelm
# Date 1689493842 -7200
# Node ID 10f8f12c61b080fae5d6bb0f25319608f564f113
# Parent  9f2cfb9873bbddf70b8f0eab03c2c80365cf0213
proper close() operation;

diff -r 9f2cfb9873bb -r 10f8f12c61b0 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Jul 16 09:34:30 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Sun Jul 16 09:50:42 2023 +0200
@@ -883,12 +883,13 @@
               db2.using_statement(table.insert()) { stmt2 =>
                 db.using_statement(
                   Data.recent_pull_date_table(days, afp_rev = afp_rev).query) { stmt =>
-                  val res = stmt.execute_query()
-                  while (res.next()) {
-                    for ((c, i) <- table.columns.zipWithIndex) {
-                      stmt2.string(i + 1) = res.get_string(c)
+                  using(stmt.execute_query()) { res =>
+                    while (res.next()) {
+                      for ((c, i) <- table.columns.zipWithIndex) {
+                        stmt2.string(i + 1) = res.get_string(c)
+                      }
+                      stmt2.execute()
                     }
-                    stmt2.execute()
                   }
                 }
               }
diff -r 9f2cfb9873bb -r 10f8f12c61b0 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun Jul 16 09:34:30 2023 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun Jul 16 09:50:42 2023 +0200
@@ -259,90 +259,91 @@
         progress.echo(sql, verbose = true)
 
         db.using_statement(sql) { stmt =>
-          val res = stmt.execute_query()
-          while (res.next()) {
-            val session_name = res.string(Build_Log.Data.session_name)
-            val chapter = res.string(Build_Log.Data.chapter)
-            val groups = split_lines(res.string(Build_Log.Data.groups))
-            val threads = {
-              val threads1 =
-                res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
-                  case Threads_Option(Value.Int(i)) => i
-                  case _ => 1
-                }
-              val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
-              threads1 max threads2
-            }
-            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
-            val ml_platform_64 =
-              ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-")
-            val data_name =
-              profile.description +
-                (if (ml_platform_64) ", 64bit" else "") +
-                (if (threads == 1) "" else ", " + threads + " threads")
+          using(stmt.execute_query()) { res =>
+            while (res.next()) {
+              val session_name = res.string(Build_Log.Data.session_name)
+              val chapter = res.string(Build_Log.Data.chapter)
+              val groups = split_lines(res.string(Build_Log.Data.groups))
+              val threads = {
+                val threads1 =
+                  res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
+                    case Threads_Option(Value.Int(i)) => i
+                    case _ => 1
+                  }
+                val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
+                threads1 max threads2
+              }
+              val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
+              val ml_platform_64 =
+                ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-")
+              val data_name =
+                profile.description +
+                  (if (ml_platform_64) ", 64bit" else "") +
+                  (if (threads == 1) "" else ", " + threads + " threads")
 
-            res.get_string(Build_Log.Prop.build_host).foreach(host =>
-              data_hosts += (data_name -> (get_hosts(data_name) + host)))
+              res.get_string(Build_Log.Prop.build_host).foreach(host =>
+                data_hosts += (data_name -> (get_hosts(data_name) + host)))
 
-            data_stretch += (data_name -> profile.stretch(options))
+              data_stretch += (data_name -> profile.stretch(options))
 
-            val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
-            val afp_version = res.string(Build_Log.Prop.afp_version)
+              val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
+              val afp_version = res.string(Build_Log.Prop.afp_version)
 
-            val ml_stats =
-              ML_Statistics(
-                if (ml_statistics) {
-                  Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
-                }
-                else Nil,
-                domain = ml_statistics_domain,
-                heading = session_name + print_version(isabelle_version, afp_version, chapter))
+              val ml_stats =
+                ML_Statistics(
+                  if (ml_statistics) {
+                    Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
+                  }
+                  else Nil,
+                  domain = ml_statistics_domain,
+                  heading = session_name + print_version(isabelle_version, afp_version, chapter))
 
-            val entry =
-              Entry(
-                chapter = chapter,
-                pull_date = res.date(Build_Log.Data.pull_date(afp = false)),
-                afp_pull_date =
-                  if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None,
-                isabelle_version = isabelle_version,
-                afp_version = afp_version,
-                timing =
-                  res.timing(
-                    Build_Log.Data.timing_elapsed,
-                    Build_Log.Data.timing_cpu,
-                    Build_Log.Data.timing_gc),
-                ml_timing =
-                  res.timing(
-                    Build_Log.Data.ml_timing_elapsed,
-                    Build_Log.Data.ml_timing_cpu,
-                    Build_Log.Data.ml_timing_gc),
-                maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)),
-                average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)),
-                maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)),
-                average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)),
-                maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)),
-                average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)),
-                stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)),
-                status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
-                errors =
-                  Build_Log.uncompress_errors(
-                    res.bytes(Build_Log.Data.errors), cache = store.cache))
+              val entry =
+                Entry(
+                  chapter = chapter,
+                  pull_date = res.date(Build_Log.Data.pull_date(afp = false)),
+                  afp_pull_date =
+                    if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None,
+                  isabelle_version = isabelle_version,
+                  afp_version = afp_version,
+                  timing =
+                    res.timing(
+                      Build_Log.Data.timing_elapsed,
+                      Build_Log.Data.timing_cpu,
+                      Build_Log.Data.timing_gc),
+                  ml_timing =
+                    res.timing(
+                      Build_Log.Data.ml_timing_elapsed,
+                      Build_Log.Data.ml_timing_cpu,
+                      Build_Log.Data.ml_timing_gc),
+                  maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)),
+                  average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)),
+                  maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)),
+                  average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)),
+                  maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)),
+                  average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)),
+                  stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)),
+                  status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
+                  errors =
+                    Build_Log.uncompress_errors(
+                      res.bytes(Build_Log.Data.errors), cache = store.cache))
 
-            val sessions = data_entries.getOrElse(data_name, Map.empty)
-            val session =
-              sessions.get(session_name) match {
-                case None =>
-                  Session(session_name, threads, List(entry), ml_stats, entry.date)
-                case Some(old) =>
-                  val (ml_stats1, ml_stats1_date) =
-                    if (entry.date > old.ml_statistics_date) (ml_stats, entry.date)
-                    else (old.ml_statistics, old.ml_statistics_date)
-                  Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
+              val sessions = data_entries.getOrElse(data_name, Map.empty)
+              val session =
+                sessions.get(session_name) match {
+                  case None =>
+                    Session(session_name, threads, List(entry), ml_stats, entry.date)
+                  case Some(old) =>
+                    val (ml_stats1, ml_stats1_date) =
+                      if (entry.date > old.ml_statistics_date) (ml_stats, entry.date)
+                      else (old.ml_statistics, old.ml_statistics_date)
+                    Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
+                }
+
+              if ((!afp || chapter == AFP.chapter) &&
+                  (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
+                data_entries += (data_name -> (sessions + (session_name -> session)))
               }
-
-            if ((!afp || chapter == AFP.chapter) &&
-                (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
-              data_entries += (data_name -> (sessions + (session_name -> session)))
             }
           }
         }
diff -r 9f2cfb9873bb -r 10f8f12c61b0 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 09:34:30 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 09:50:42 2023 +0200
@@ -331,7 +331,7 @@
 
   /* results */
 
-  class Result private[SQL](val stmt: Statement, val rep: ResultSet) {
+  class Result private[SQL](val stmt: Statement, val rep: ResultSet) extends AutoCloseable {
     res =>
 
     def next(): Boolean = rep.next()
@@ -370,6 +370,8 @@
     def get_string(column: Column): Option[String] = get(column, string)
     def get_bytes(column: Column): Option[Bytes] = get(column, bytes)
     def get_date(column: Column): Option[Date] = get(column, date)
+
+    override def close(): Unit = rep.close()
   }
 
 
@@ -471,13 +473,17 @@
       sql: Source,
       make_result: Iterator[A] => B,
       get: Result => A
-    ): B = using_statement(sql)(stmt => make_result(stmt.execute_query().iterator(get)))
+    ): B = {
+      using_statement(sql) { stmt =>
+        using(stmt.execute_query()) { res => make_result(res.iterator(get)) }
+      }
+    }
 
     def execute_query_statementO[A](sql: Source, get: Result => A): Option[A] =
       execute_query_statement[A, Option[A]](sql, _.nextOption, get)
 
     def execute_query_statementB(sql: Source): Boolean =
-      using_statement(sql)(stmt => stmt.execute_query().next())
+      using_statement(sql)(stmt => using(stmt.execute_query())(_.next()))
 
     def update_date(stmt: Statement, i: Int, date: Date): Unit
     def date(res: Result, column: Column): Date