src/Pure/Admin/build_status.scala
changeset 67003 49850a679c2c
parent 67002 e8d64340d58b
child 67738 1bbe618c4b24
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat Nov 04 14:41:26 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat Nov 04 15:24:40 2017 +0100
     1.3 @@ -79,13 +79,13 @@
     1.4    {
     1.5      require(entries.nonEmpty)
     1.6  
     1.7 -    def sort_entries: Session =
     1.8 -      copy(entries = entries.sortBy(entry => - entry.pull_date.unix_epoch))
     1.9 +    lazy val sorted_entries: List[Entry] =
    1.10 +      entries.sortBy(entry => - entry.pull_date.unix_epoch)
    1.11  
    1.12 -    def head: Entry = entries.head
    1.13 +    def head: Entry = sorted_entries.head
    1.14      def order: Long = - head.timing.elapsed.ms
    1.15  
    1.16 -    def finished_entries: List[Entry] = entries.filter(_.finished)
    1.17 +    def finished_entries: List[Entry] = sorted_entries.filter(_.finished)
    1.18      def finished_entries_size: Int =
    1.19        finished_entries.map(entry => entry.pull_date.unix_epoch).toSet.size
    1.20  
    1.21 @@ -263,7 +263,7 @@
    1.22      val sorted_entries =
    1.23        (for {
    1.24          (name, sessions) <- data_entries.toList
    1.25 -        sorted_sessions <- proper_list(sessions.toList.map(p => p._2.sort_entries).sortBy(_.order))
    1.26 +        sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
    1.27        }
    1.28        yield {
    1.29          val hosts = get_hosts(name).toList.sorted