tuned;
authorwenzelm
Fri May 12 11:56:41 2017 +0200 (2017-05-12)
changeset 6580473ed0ebac3b0
parent 65803 1fdb6ba9d32c
child 65805 d3c5898f1a5e
tuned;
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_status.scala
src/Pure/General/sql.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Wed May 10 22:30:28 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri May 12 11:56:41 2017 +0200
     1.3 @@ -983,10 +983,7 @@
     1.4          Data.session_name(table1) + " <> ''"
     1.5        val where =
     1.6          if (session_names.isEmpty) where_log_name
     1.7 -        else
     1.8 -          where_log_name + " AND " +
     1.9 -          session_names.map(a => Data.session_name(table1) + " = " + SQL.string(a)).
    1.10 -            mkString("(", " OR ", ")")
    1.11 +        else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
    1.12  
    1.13        val columns1 = table1.columns.tail.map(_.apply(table1))
    1.14        val (columns, from) =
     2.1 --- a/src/Pure/Admin/build_status.scala	Wed May 10 22:30:28 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_status.scala	Fri May 12 11:56:41 2017 +0200
     2.3 @@ -30,17 +30,13 @@
     2.4  
     2.5      def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source =
     2.6      {
     2.7 -      val sql_sessions =
     2.8 -        if (only_sessions.isEmpty) ""
     2.9 -        else
    2.10 -          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
    2.11 -            .mkString("(", " OR ", ") AND ")
    2.12 -
    2.13        Build_Log.Data.universal_table.select(columns, distinct = true,
    2.14          sql = "WHERE " +
    2.15            Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " +
    2.16            Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    2.17 -          " AND " + sql_sessions + SQL.enclose(sql) +
    2.18 +          (if (only_sessions.isEmpty) ""
    2.19 +           else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
    2.20 +          " AND " + SQL.enclose(sql) +
    2.21            " ORDER BY " + Build_Log.Data.pull_date + " DESC")
    2.22      }
    2.23    }
     3.1 --- a/src/Pure/General/sql.scala	Wed May 10 22:30:28 2017 +0200
     3.2 +++ b/src/Pure/General/sql.scala	Fri May 12 11:56:41 2017 +0200
     3.3 @@ -52,6 +52,9 @@
     3.4    val join_inner: Source = " INNER JOIN "
     3.5    def join(outer: Boolean): Source = if (outer) join_outer else join_inner
     3.6  
     3.7 +  def member(x: Source, set: Iterable[String]): Source =
     3.8 +    set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
     3.9 +
    3.10  
    3.11    /* types */
    3.12