proper order for entries from multiple profiles, notably "AFP";
authorwenzelm
Wed Nov 01 18:24:39 2017 +0100 (7 months ago)
changeset 66981e76c6cb0d461
parent 66980 8947cf58cb86
child 66982 67595389aa8a
proper order for entries from multiple profiles, notably "AFP";
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed Nov 01 17:29:14 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed Nov 01 18:24:39 2017 +0100
     1.3 @@ -41,8 +41,7 @@
     1.4                Build_Log.Session_Status.failed.toString)) +
     1.5            (if (only_sessions.isEmpty) ""
     1.6             else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
     1.7 -          " AND " + SQL.enclose(sql) +
     1.8 -          " ORDER BY " + Build_Log.Data.pull_date(afp))
     1.9 +          " AND " + SQL.enclose(sql))
    1.10      }
    1.11    }
    1.12  
    1.13 @@ -80,6 +79,9 @@
    1.14    {
    1.15      require(entries.nonEmpty)
    1.16  
    1.17 +    def sort_entries: Session =
    1.18 +      copy(entries = entries.sortBy(entry => - entry.pull_date.unix_epoch))
    1.19 +
    1.20      def head: Entry = entries.head
    1.21      def order: Long = - head.timing.elapsed.ms
    1.22  
    1.23 @@ -261,7 +263,7 @@
    1.24      val sorted_entries =
    1.25        (for {
    1.26          (name, sessions) <- data_entries.toList
    1.27 -        sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
    1.28 +        sorted_sessions <- proper_list(sessions.toList.map(p => p._2.sort_entries).sortBy(_.order))
    1.29        }
    1.30        yield {
    1.31          val hosts = get_hosts(name).toList.sorted