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