--- a/src/Pure/Admin/build_log.scala Wed May 10 22:30:28 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Fri May 12 11:56:41 2017 +0200
@@ -983,10 +983,7 @@
Data.session_name(table1) + " <> ''"
val where =
if (session_names.isEmpty) where_log_name
- else
- where_log_name + " AND " +
- session_names.map(a => Data.session_name(table1) + " = " + SQL.string(a)).
- mkString("(", " OR ", ")")
+ else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
val columns1 = table1.columns.tail.map(_.apply(table1))
val (columns, from) =
--- a/src/Pure/Admin/build_status.scala Wed May 10 22:30:28 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Fri May 12 11:56:41 2017 +0200
@@ -30,17 +30,13 @@
def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source =
{
- val sql_sessions =
- if (only_sessions.isEmpty) ""
- else
- only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
- .mkString("(", " OR ", ") AND ")
-
Build_Log.Data.universal_table.select(columns, distinct = true,
sql = "WHERE " +
Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " +
Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
- " AND " + sql_sessions + SQL.enclose(sql) +
+ (if (only_sessions.isEmpty) ""
+ else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
+ " AND " + SQL.enclose(sql) +
" ORDER BY " + Build_Log.Data.pull_date + " DESC")
}
}
--- a/src/Pure/General/sql.scala Wed May 10 22:30:28 2017 +0200
+++ b/src/Pure/General/sql.scala Fri May 12 11:56:41 2017 +0200
@@ -52,6 +52,9 @@
val join_inner: Source = " INNER JOIN "
def join(outer: Boolean): Source = if (outer) join_outer else join_inner
+ def member(x: Source, set: Iterable[String]): Source =
+ set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+
/* types */