# HG changeset patch
# User wenzelm
# Date 1494583001 -7200
# Node ID 73ed0ebac3b0565cbe4036fc325261b032e3128b
# Parent  1fdb6ba9d32c655670365d0beee49622ae41e3f1
tuned;

diff -r 1fdb6ba9d32c -r 73ed0ebac3b0 src/Pure/Admin/build_log.scala
--- 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) =
diff -r 1fdb6ba9d32c -r 73ed0ebac3b0 src/Pure/Admin/build_status.scala
--- 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")
     }
   }
diff -r 1fdb6ba9d32c -r 73ed0ebac3b0 src/Pure/General/sql.scala
--- 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 */