# HG changeset patch
# User wenzelm
# Date 1678115184 -3600
# Node ID 42c1e5d4ed1479624417d14ef4056b04ceccad13
# Parent  97b5547f2b17b0af00e7c247fb17d863b7165104
tuned: prefer iterator.nextOption;

diff -r 97b5547f2b17 -r 42c1e5d4ed14 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 06 15:56:28 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 06 16:06:24 2023 +0100
@@ -1027,9 +1027,7 @@
       val table = Data.meta_info_table
       val columns = table.columns.tail
       db.using_statement(table.select(columns, sql = Data.log_name.where_equal(log_name))) { stmt =>
-        val res = stmt.execute_query()
-        if (!res.next()) None
-        else {
+        (stmt.execute_query().iterator { res =>
           val results =
             columns.map(c => c.name ->
               (if (c.T == SQL.Type.Date)
@@ -1039,8 +1037,8 @@
           val n = Prop.all_props.length
           val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
           val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
-          Some(Meta_Info(props, settings))
-        }
+          Meta_Info(props, settings)
+        }).nextOption
       }
     }
 
diff -r 97b5547f2b17 -r 42c1e5d4ed14 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Mar 06 15:56:28 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Mar 06 16:06:24 2023 +0100
@@ -87,15 +87,13 @@
     name: String
   ): Option[Document_Output] = {
     db.using_statement(Data.table.select(sql = Data.where_equal(session_name, name))) { stmt =>
-      val res = stmt.execute_query()
-      if (res.next()) {
+      (stmt.execute_query().iterator { res =>
         val name = res.string(Data.name)
         val sources = res.string(Data.sources)
         val log_xz = res.bytes(Data.log_xz)
         val pdf = res.bytes(Data.pdf)
-        Some(Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf))
-      }
-      else None
+        Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
+      }).nextOption
     }
   }
 
diff -r 97b5547f2b17 -r 42c1e5d4ed14 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Mar 06 15:56:28 2023 +0100
+++ b/src/Pure/Thy/export.scala	Mon Mar 06 16:06:24 2023 +0100
@@ -73,15 +73,13 @@
       db.using_statement(
         Data.table.select(List(Data.executable, Data.compressed, Data.body),
           sql = Data.where_equal(session, theory, name))) { stmt =>
-        val res = stmt.execute_query()
-        if (res.next()) {
+        (stmt.execute_query().iterator { res =>
           val executable = res.bool(Data.executable)
           val compressed = res.bool(Data.compressed)
           val bytes = res.bytes(Data.body)
           val body = Future.value(compressed, bytes)
-          Some(Entry(this, executable, body, cache))
-        }
-        else None
+          Entry(this, executable, body, cache)
+        }).nextOption
       }
   }
 
diff -r 97b5547f2b17 -r 42c1e5d4ed14 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 06 15:56:28 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 06 16:06:24 2023 +0100
@@ -1634,20 +1634,17 @@
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(
           Session_Info.table.select(sql = Session_Info.session_name.where_equal(name))) { stmt =>
-          val res = stmt.execute_query()
-          if (!res.next()) None
-          else {
+          (stmt.execute_query().iterator { res =>
             val uuid =
               try { Option(res.string(Session_Info.uuid)).getOrElse("") }
               catch { case _: SQLException => "" }
-            Some(
-              Build_Info(
-                SHA1.fake_shasum(res.string(Session_Info.sources)),
-                SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
-                SHA1.fake_shasum(res.string(Session_Info.output_heap)),
-                res.int(Session_Info.return_code),
-                uuid))
-          }
+            Build_Info(
+              SHA1.fake_shasum(res.string(Session_Info.sources)),
+              SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
+              SHA1.fake_shasum(res.string(Session_Info.output_heap)),
+              res.int(Session_Info.return_code),
+              uuid)
+          }).nextOption
         }
       }
       else None