# HG changeset patch
# User wenzelm
# Date 1509805480 -3600
# Node ID 49850a679c2c8de0be825a22371983e3938a92ef
# Parent  e8d64340d58bafd34d84d4a22df88234164197cb
more robust sorted_entries;

diff -r e8d64340d58b -r 49850a679c2c src/Pure/Admin/build_status.scala
--- 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