--- a/src/Pure/Admin/build_log.scala Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Sun Feb 26 13:50:07 2023 +0100
@@ -1068,7 +1068,7 @@
Data.session_name(table1) + " <> ''"
val where =
if (session_names.isEmpty) where_log_name
- else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
+ else where_log_name + " AND " + Data.session_name(table1).member(session_names)
val columns1 = table1.columns.tail.map(_.apply(table1))
val (columns, from) =
--- a/src/Pure/Admin/build_status.scala Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/build_status.scala Sun Feb 26 13:50:07 2023 +0100
@@ -40,12 +40,11 @@
sql = "WHERE " +
Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
" AND " +
- SQL.member(Build_Log.Data.status.ident,
+ Build_Log.Data.status.member(
List(
Build_Log.Session_Status.finished.toString,
Build_Log.Session_Status.failed.toString)) +
- if_proper(only_sessions,
- " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
+ if_proper(only_sessions, " AND " + Build_Log.Data.session_name.member(only_sessions)) +
" AND " + SQL.enclose(sql))
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Feb 26 13:50:07 2023 +0100
@@ -156,8 +156,8 @@
def sql: PostgreSQL.Source =
SQL.and(
- Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine),
- SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts),
+ Build_Log.Prop.build_engine.equal(Build_History.engine),
+ Build_Log.Prop.build_host.member(host :: more_hosts),
if_proper(detect, SQL.enclose(detect)))
def profile: Build_Status.Profile =
--- a/src/Pure/General/sql.scala Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/General/sql.scala Sun Feb 26 13:50:07 2023 +0100
@@ -69,16 +69,15 @@
val TRUE: Source = "TRUE"
val FALSE: Source = "FALSE"
- def member(x: Source, set: Iterable[String]): Source =
+ def equal(sql: Source, s: String): Source = sql + " = " + string(s)
+
+ def member(sql: Source, set: Iterable[String]): Source =
if (set.isEmpty) FALSE
- else OR(set.iterator.map(a => x + " = " + SQL.string(a)).toList)
-
- def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
+ else OR(set.iterator.map(equal(sql, _)).toList)
def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
-
/* types */
object Type extends Enumeration {
@@ -144,8 +143,11 @@
def defined: String = ident + " IS NOT NULL"
def undefined: String = ident + " IS NULL"
- def equal(s: String): Source = ident + " = " + string(s)
- def where_equal(s: String): Source = " WHERE " + equal(s)
+ def equal(s: String): Source = SQL.equal(ident, s)
+ def member(set: Iterable[String]): Source = SQL.member(ident, set)
+
+ def where_equal(s: String): Source = SQL.where(equal(s))
+ def where_member(set: Iterable[String]): Source = SQL.where(member(set))
override def toString: Source = ident
}
--- a/src/Pure/Tools/build_process.scala Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sun Feb 26 13:50:07 2023 +0100
@@ -246,7 +246,7 @@
def sql_member(instance: String = "", names: Iterable[String] = Nil): SQL.Source =
SQL.and(
if_proper(instance, Generic.instance.equal(instance)),
- if_proper(names, SQL.member(Generic.name.toString, names)))
+ if_proper(names, Generic.name.member(names)))
}
object Config {
@@ -367,7 +367,7 @@
def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
db.using_statement(
- Results.table.select() + if_proper(names, SQL.where_member(Results.name.toString, names))
+ Results.table.select() + if_proper(names, Results.name.where_member(names))
) { stmt =>
Map.from(
stmt.execute_query().iterator { res =>