--- a/src/Pure/Admin/build_status.scala Sat Nov 04 14:41:26 2017 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Nov 04 15:24:40 2017 +0100
@@ -79,13 +79,13 @@
{
require(entries.nonEmpty)
- def sort_entries: Session =
- copy(entries = entries.sortBy(entry => - entry.pull_date.unix_epoch))
+ lazy val sorted_entries: List[Entry] =
+ entries.sortBy(entry => - entry.pull_date.unix_epoch)
- def head: Entry = entries.head
+ def head: Entry = sorted_entries.head
def order: Long = - head.timing.elapsed.ms
- def finished_entries: List[Entry] = entries.filter(_.finished)
+ def finished_entries: List[Entry] = sorted_entries.filter(_.finished)
def finished_entries_size: Int =
finished_entries.map(entry => entry.pull_date.unix_epoch).toSet.size
@@ -263,7 +263,7 @@
val sorted_entries =
(for {
(name, sessions) <- data_entries.toList
- sorted_sessions <- proper_list(sessions.toList.map(p => p._2.sort_entries).sortBy(_.order))
+ sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
}
yield {
val hosts = get_hosts(name).toList.sorted