--- a/src/Pure/Admin/build_log.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Mar 06 21:12:47 2023 +0100
@@ -864,8 +864,9 @@
db2.create_table(Data.ml_statistics_table)
val recent_log_names =
- db.using_statement(Data.select_recent_log_names(days))(stmt =>
- stmt.execute_query().iterator(_.string(Data.log_name)).toList)
+ db.execute_query_statement(
+ Data.select_recent_log_names(days),
+ List.from[String], res => res.string(Data.log_name))
for (log_name <- recent_log_names) {
read_meta_info(db, log_name).foreach(meta_info =>
@@ -907,8 +908,9 @@
}
def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
- db.using_statement(table.select(List(column), distinct = true))(stmt =>
- stmt.execute_query().iterator(_.string(column)).toSet)
+ db.execute_query_statement(
+ table.select(List(column), distinct = true),
+ Set.from[String], res => res.string(column))
def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
db.execute_statement(db.insert_permissive(Data.meta_info_table), body =
@@ -1030,8 +1032,9 @@
def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
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 =>
- (stmt.execute_query().iterator { res =>
+ db.execute_query_statementO[Meta_Info](
+ table.select(columns, sql = Data.log_name.where_equal(log_name)),
+ { res =>
val results =
columns.map(c => c.name ->
(if (c.T == SQL.Type.Date)
@@ -1042,8 +1045,8 @@
val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
Meta_Info(props, settings)
- }).nextOption
- }
+ }
+ )
}
def read_build_info(
@@ -1076,8 +1079,10 @@
if_proper(session_names, Data.session_name(table1).member(session_names))))
val sessions =
- db.using_statement(SQL.select(columns, sql = from + where)) { stmt =>
- stmt.execute_query().iterator({ res =>
+ db.execute_query_statement(
+ SQL.select(columns, sql = from + where),
+ Map.from[String, Session_Entry],
+ { res =>
val session_name = res.string(Data.session_name)
val session_entry =
Session_Entry(
@@ -1104,8 +1109,8 @@
}
else Nil)
session_name -> session_entry
- }).toMap
- }
+ }
+ )
Build_Info(sessions)
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 06 21:12:47 2023 +0100
@@ -113,18 +113,18 @@
sql: PostgreSQL.Source
): List[Item] = {
val afp = afp_rev.isDefined
- val select =
+
+ db.execute_query_statement(
Build_Log.Data.select_recent_versions(
- days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
-
- db.using_statement(select)(stmt =>
- stmt.execute_query().iterator({ res =>
+ days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql),
+ List.from[Item],
+ { res =>
val known = res.bool(Build_Log.Data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
val pull_date = res.date(Build_Log.Data.pull_date(afp))
Item(known, isabelle_version, afp_version, pull_date)
- }).toList)
+ })
}
def unknown_runs(items: List[Item]): List[List[Item]] = {
--- a/src/Pure/General/sql.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/General/sql.scala Mon Mar 06 21:12:47 2023 +0100
@@ -381,6 +381,18 @@
def execute_statement(sql: Source, body: Statement => Unit = _ => ()): Unit =
using_statement(sql) { stmt => body(stmt); stmt.execute() }
+ def execute_query_statement[A, B](
+ sql: Source,
+ make_result: Iterator[A] => B,
+ get: Result => A
+ ): B = using_statement(sql)(stmt => make_result(stmt.execute_query().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())
+
def update_date(stmt: Statement, i: Int, date: Date): Unit
def date(res: Result, column: Column): Date
@@ -518,9 +530,8 @@
override def now(): Date = {
val now = SQL.Column.date("now")
- using_statement("SELECT NOW() as " + now.ident)(
- stmt => stmt.execute_query().iterator(_.date(now)).nextOption
- ).getOrElse(error("Failed to get current date/time from database server " + toString))
+ execute_query_statementO[Date]("SELECT NOW() as " + now.ident, res => res.date(now))
+ .getOrElse(error("Failed to get current date/time from database server " + toString))
}
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
--- a/src/Pure/System/host.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 21:12:47 2023 +0100
@@ -107,10 +107,11 @@
}
def read_numa_next(db: SQL.Database, hostname: String): Int =
- db.using_statement(
+ db.execute_query_statementO[Int](
Node_Info.table.select(List(Node_Info.numa_next),
- sql = Node_Info.hostname.where_equal(hostname))
- )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_next)).nextOption.getOrElse(0))
+ sql = Node_Info.hostname.where_equal(hostname)),
+ res => res.int(Node_Info.numa_next)
+ ).getOrElse(0)
def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
if (read_numa_next(db, hostname) != numa_next) {
--- a/src/Pure/Thy/document_build.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Mon Mar 06 21:12:47 2023 +0100
@@ -71,30 +71,31 @@
}
def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
- db.using_statement(
- Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name))
- ) { stmt =>
- (stmt.execute_query().iterator { res =>
- val name = res.string(Data.name)
- val sources = res.string(Data.sources)
- Document_Input(name, SHA1.fake_shasum(sources))
- }).toList
+ db.execute_query_statement(
+ Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name)),
+ List.from[Document_Input],
+ { res =>
+ val name = res.string(Data.name)
+ val sources = res.string(Data.sources)
+ Document_Input(name, SHA1.fake_shasum(sources))
}
+ )
def read_document(
db: SQL.Database,
session_name: String,
name: String
): Option[Document_Output] = {
- db.using_statement(Data.table.select(sql = Data.where_equal(session_name, name))) { stmt =>
- (stmt.execute_query().iterator { res =>
+ db.execute_query_statementO[Document_Output](
+ Data.table.select(sql = Data.where_equal(session_name, name)),
+ { 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)
Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
- }).nextOption
- }
+ }
+ )
}
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
--- a/src/Pure/Thy/export.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Thy/export.scala Mon Mar 06 21:12:47 2023 +0100
@@ -64,41 +64,42 @@
}
def readable(db: SQL.Database): Boolean = {
- db.using_statement(
+ db.execute_query_statementB(
Data.table.select(List(Data.name),
- sql = Data.where_equal(session, theory, name)))(_.execute_query().next())
+ sql = Data.where_equal(session, theory, name)))
}
def read(db: SQL.Database, cache: XML.Cache): Option[Entry] =
- db.using_statement(
+ db.execute_query_statementO[Entry](
Data.table.select(List(Data.executable, Data.compressed, Data.body),
- sql = Data.where_equal(session, theory, name))) { stmt =>
- (stmt.execute_query().iterator { res =>
+ sql = Data.where_equal(session, theory, name)),
+ { 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)
Entry(this, executable, body, cache)
- }).nextOption
- }
+ }
+ )
}
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
- db.using_statement(
+ db.execute_query_statement(
Data.table.select(List(Data.theory_name), distinct = true,
- sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name)))
- ) { stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList }
+ sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name))),
+ List.from[String], res => res.string(Data.theory_name))
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] =
- db.using_statement(
+ db.execute_query_statement(
Data.table.select(List(Data.theory_name, Data.name),
- sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name))
- ) { stmt =>
- stmt.execute_query().iterator(res =>
- Entry_Name(session = session_name,
- theory = res.string(Data.theory_name),
- name = res.string(Data.name))).toList
- }
+ sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name)),
+ List.from[Entry_Name],
+ { res =>
+ Entry_Name(
+ session = session_name,
+ theory = res.string(Data.theory_name),
+ name = res.string(Data.name))
+ })
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
--- a/src/Pure/Thy/sessions.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Mar 06 21:12:47 2023 +0100
@@ -1536,12 +1536,11 @@
/* SQL database content */
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
- db.using_statement(
+ db.execute_query_statementO[Bytes](
Session_Info.table.select(List(column),
- sql = Session_Info.session_name.where_equal(name))) { stmt =>
- val res = stmt.execute_query()
- if (!res.next()) Bytes.empty else res.bytes(column)
- }
+ sql = Session_Info.session_name.where_equal(name)),
+ res => res.bytes(column)
+ ).getOrElse(Bytes.empty)
def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
Properties.uncompress(read_bytes(db, name, column), cache = cache)
@@ -1576,11 +1575,10 @@
}
def session_info_defined(db: SQL.Database, name: String): Boolean =
- session_info_exists(db) && {
- db.using_statement(
+ session_info_exists(db) &&
+ db.execute_query_statementB(
Session_Info.table.select(List(Session_Info.session_name),
- sql = Session_Info.session_name.where_equal(name)))(_.execute_query().next())
- }
+ sql = Session_Info.session_name.where_equal(name)))
def write_session_info(
db: SQL.Database,
@@ -1632,9 +1630,9 @@
def read_build(db: SQL.Database, name: String): Option[Build_Info] = {
if (db.tables.contains(Session_Info.table.name)) {
- db.using_statement(
- Session_Info.table.select(sql = Session_Info.session_name.where_equal(name))) { stmt =>
- (stmt.execute_query().iterator { res =>
+ db.execute_query_statementO[Build_Info](
+ Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)),
+ { res =>
val uuid =
try { Option(res.string(Session_Info.uuid)).getOrElse("") }
catch { case _: SQLException => "" }
@@ -1644,8 +1642,8 @@
SHA1.fake_shasum(res.string(Session_Info.output_heap)),
res.int(Session_Info.return_code),
uuid)
- }).nextOption
- }
+ }
+ )
}
else None
}
@@ -1670,18 +1668,18 @@
session_name: String,
name: String = ""
): List[Source_File] = {
- db.using_statement(
+ db.execute_query_statement(
Sources.table.select(sql =
- Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name)))
- ) { stmt =>
- (stmt.execute_query().iterator { res =>
- val res_name = res.string(Sources.name)
- val digest = SHA1.fake_digest(res.string(Sources.digest))
- val compressed = res.bool(Sources.compressed)
- val body = res.bytes(Sources.body)
- Source_File(res_name, digest, compressed, body, cache.compress)
- }).toList
+ Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name))),
+ List.from[Source_File],
+ { res =>
+ val res_name = res.string(Sources.name)
+ val digest = SHA1.fake_digest(res.string(Sources.digest))
+ val compressed = res.bool(Sources.compressed)
+ val body = res.bytes(Sources.body)
+ Source_File(res_name, digest, compressed, body, cache.compress)
}
+ )
}
}
}
--- a/src/Pure/Tools/build_process.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 06 21:12:47 2023 +0100
@@ -304,9 +304,9 @@
def clean_build(db: SQL.Database): Unit = {
val old =
- db.using_statement(
- Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined))
- )(stmt => stmt.execute_query().iterator(_.string(Base.build_uuid)).toList)
+ db.execute_query_statement(
+ Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined)),
+ List.from[String], res => res.string(Base.build_uuid))
if (old.nonEmpty) {
for (table <- List(Base.table, Sessions.table, Progress.table, Workers.table)) {
@@ -333,26 +333,27 @@
}
def read_sessions_domain(db: SQL.Database): Set[String] =
- db.using_statement(Sessions.table.select(List(Sessions.name)))(stmt =>
- Set.from(stmt.execute_query().iterator(_.string(Sessions.name))))
+ db.execute_query_statement(
+ Sessions.table.select(List(Sessions.name)),
+ Set.from[String], res => res.string(Sessions.name))
def read_sessions(db: SQL.Database, names: Iterable[String] = Nil): State.Sessions =
- db.using_statement(
- Sessions.table.select(sql = if_proper(names, Sessions.name.where_member(names)))
- ) { stmt =>
- Map.from(stmt.execute_query().iterator { res =>
- val name = res.string(Sessions.name)
- val deps = split_lines(res.string(Sessions.deps))
- val ancestors = split_lines(res.string(Sessions.ancestors))
- val sources_shasum = SHA1.fake_shasum(res.string(Sessions.sources))
- val timeout = Time.ms(res.long(Sessions.timeout))
- val old_time = Time.ms(res.long(Sessions.old_time))
- val old_command_timings_blob = res.bytes(Sessions.old_command_timings)
- val build_uuid = res.string(Sessions.build_uuid)
- name -> Build_Job.Session_Context(name, deps, ancestors, sources_shasum,
- timeout, old_time, old_command_timings_blob, build_uuid)
- })
+ db.execute_query_statement(
+ Sessions.table.select(sql = if_proper(names, Sessions.name.where_member(names))),
+ Map.from[String, Build_Job.Session_Context],
+ { res =>
+ val name = res.string(Sessions.name)
+ val deps = split_lines(res.string(Sessions.deps))
+ val ancestors = split_lines(res.string(Sessions.ancestors))
+ val sources_shasum = SHA1.fake_shasum(res.string(Sessions.sources))
+ val timeout = Time.ms(res.long(Sessions.timeout))
+ val old_time = Time.ms(res.long(Sessions.old_time))
+ val old_command_timings_blob = res.bytes(Sessions.old_command_timings)
+ val build_uuid = res.string(Sessions.build_uuid)
+ name -> Build_Job.Session_Context(name, deps, ancestors, sources_shasum,
+ timeout, old_time, old_command_timings_blob, build_uuid)
}
+ )
def update_sessions(db:SQL.Database, sessions: State.Sessions): Boolean = {
val old_sessions = read_sessions_domain(db)
@@ -389,22 +390,22 @@
}
def read_progress(db: SQL.Database, seen: Long = 0, build_uuid: String = ""): Progress_Messages =
- db.using_statement(
+ db.execute_query_statement(
Progress.table.select(
sql =
SQL.where(
SQL.and(
if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
- Generic.sql(build_uuid = build_uuid))))
- ) { stmt =>
- SortedMap.from(stmt.execute_query().iterator { res =>
- val serial = res.long(Progress.serial)
- val kind = isabelle.Progress.Kind(res.int(Progress.kind))
- val text = res.string(Progress.text)
- val verbose = res.bool(Progress.verbose)
- serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
- })
+ Generic.sql(build_uuid = build_uuid)))),
+ SortedMap.from[Long, isabelle.Progress.Message],
+ { res =>
+ val serial = res.long(Progress.serial)
+ val kind = isabelle.Progress.Kind(res.int(Progress.kind))
+ val text = res.string(Progress.text)
+ val verbose = res.bool(Progress.verbose)
+ serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
}
+ )
def write_progress(
db: SQL.Database,
@@ -439,20 +440,21 @@
}
def serial_max(db: SQL.Database): Long =
- db.using_statement(
- Workers.table.select(List(Workers.serial_max))
- )(stmt => stmt.execute_query().iterator(_.long(Workers.serial)).nextOption.getOrElse(0L))
+ db.execute_query_statementO[Long](
+ Workers.table.select(List(Workers.serial_max)),
+ res => res.long(Workers.serial)
+ ).getOrElse(0L)
def start_worker(db: SQL.Database, worker_uuid: String, build_uuid: String): Long = {
def err(msg: String): Nothing =
error("Cannot start worker " + worker_uuid + if_proper(msg, "\n" + msg))
- val build_stop = {
- val sql =
+ val build_stop =
+ db.execute_query_statementO(
Base.table.select(List(Base.stop),
- sql = SQL.where(Generic.sql(build_uuid = build_uuid)))
- db.using_statement(sql)(_.execute_query().iterator(_.get_date(Base.stop)).nextOption)
- }
+ sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+ res => res.get_date(Base.stop))
+
build_stop match {
case Some(None) =>
case Some(Some(_)) => err("for already stopped build process " + build_uuid)
@@ -503,15 +505,15 @@
}
def read_pending(db: SQL.Database): List[Entry] =
- db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt =>
- List.from(
- stmt.execute_query().iterator { res =>
- val name = res.string(Pending.name)
- val deps = res.string(Pending.deps)
- val info = res.string(Pending.info)
- Entry(name, split_lines(deps), info = JSON.Object.parse(info))
- })
- }
+ db.execute_query_statement(
+ Pending.table.select(sql = SQL.order_by(List(Pending.name))),
+ List.from[Entry],
+ { res =>
+ val name = res.string(Pending.name)
+ val deps = res.string(Pending.deps)
+ val info = res.string(Pending.info)
+ Entry(name, split_lines(deps), info = JSON.Object.parse(info))
+ })
def update_pending(db: SQL.Database, pending: State.Pending): Boolean = {
val old_pending = read_pending(db)
@@ -546,15 +548,16 @@
}
def read_running(db: SQL.Database): List[Build_Job.Abstract] =
- db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt =>
- List.from(
- stmt.execute_query().iterator { res =>
- val name = res.string(Running.name)
- val hostname = res.string(Running.hostname)
- val numa_node = res.get_int(Running.numa_node)
- Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node))
- })
- }
+ db.execute_query_statement(
+ Running.table.select(sql = SQL.order_by(List(Running.name))),
+ List.from[Build_Job.Abstract],
+ { res =>
+ val name = res.string(Running.name)
+ val hostname = res.string(Running.hostname)
+ val numa_node = res.get_int(Running.numa_node)
+ Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node))
+ }
+ )
def update_running(db: SQL.Database, running: State.Running): Boolean = {
val old_running = read_running(db)
@@ -599,34 +602,35 @@
}
def read_results_domain(db: SQL.Database): Set[String] =
- db.using_statement(Results.table.select(List(Results.name)))(stmt =>
- Set.from(stmt.execute_query().iterator(_.string(Results.name))))
+ db.execute_query_statement(
+ Results.table.select(List(Results.name)),
+ Set.from[String], res => res.string(Results.name))
def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
- db.using_statement(
- Results.table.select(sql = if_proper(names, Results.name.where_member(names)))
- ) { stmt =>
- Map.from(stmt.execute_query().iterator { res =>
- val name = res.string(Results.name)
- val hostname = res.string(Results.hostname)
- val numa_node = res.get_int(Results.numa_node)
- val rc = res.int(Results.rc)
- val out = res.string(Results.out)
- val err = res.string(Results.err)
- val timing =
- res.timing(
- Results.timing_elapsed,
- Results.timing_cpu,
- Results.timing_gc)
- val node_info = Host.Node_Info(hostname, numa_node)
- val process_result =
- Process_Result(rc,
- out_lines = split_lines(out),
- err_lines = split_lines(err),
- timing = timing)
- name -> Build_Job.Result(node_info, process_result)
- })
+ db.execute_query_statement(
+ Results.table.select(sql = if_proper(names, Results.name.where_member(names))),
+ Map.from[String, Build_Job.Result],
+ { res =>
+ val name = res.string(Results.name)
+ val hostname = res.string(Results.hostname)
+ val numa_node = res.get_int(Results.numa_node)
+ val rc = res.int(Results.rc)
+ val out = res.string(Results.out)
+ val err = res.string(Results.err)
+ val timing =
+ res.timing(
+ Results.timing_elapsed,
+ Results.timing_cpu,
+ Results.timing_gc)
+ val node_info = Host.Node_Info(hostname, numa_node)
+ val process_result =
+ Process_Result(rc,
+ out_lines = split_lines(out),
+ err_lines = split_lines(err),
+ timing = timing)
+ name -> Build_Job.Result(node_info, process_result)
}
+ )
def update_results(db: SQL.Database, results: State.Results): Boolean = {
val old_results = read_results_domain(db)
--- a/src/Pure/Tools/server.scala Mon Mar 06 19:37:32 2023 +0100
+++ b/src/Pure/Tools/server.scala Mon Mar 06 21:12:47 2023 +0100
@@ -374,13 +374,15 @@
def list(db: SQLite.Database): List[Info] =
if (db.tables.contains(Data.table.name)) {
- db.using_statement(Data.table.select()) { stmt =>
- stmt.execute_query().iterator(res =>
- Info(
- res.string(Data.name),
- res.int(Data.port),
- res.string(Data.password))).toList.sortBy(_.name)
- }
+ db.execute_query_statement(Data.table.select(),
+ List.from[Info],
+ { res =>
+ val name = res.string(Data.name)
+ val port = res.int(Data.port)
+ val password = res.string(Data.password)
+ Info(name, port, password)
+ }
+ ).sortBy(_.name)
}
else Nil