src/Pure/Admin/build_status.scala
changeset 67759 56eba30e7b99
parent 67749 08dc76bf6400
child 67760 553d9ad7d679
equal deleted inserted replaced
67758:9494fcf124ab 67759:56eba30e7b99
    73   {
    73   {
    74     def failed_sessions: List[Session] =
    74     def failed_sessions: List[Session] =
    75       sessions.filter(_.head.failed).sortBy(_.name)
    75       sessions.filter(_.head.failed).sortBy(_.name)
    76   }
    76   }
    77   sealed case class Session(
    77   sealed case class Session(
    78     name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
    78     name: String, threads: Int, entries: List[Entry],
       
    79     ml_statistics: ML_Statistics, ml_statistics_date: Long)
    79   {
    80   {
    80     require(entries.nonEmpty)
    81     require(entries.nonEmpty)
    81 
    82 
    82     lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date)
    83     lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date)
    83 
    84 
   293                 stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
   294                 stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
   294                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
   295                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
   295                 errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors)))
   296                 errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors)))
   296 
   297 
   297             val sessions = data_entries.getOrElse(data_name, Map.empty)
   298             val sessions = data_entries.getOrElse(data_name, Map.empty)
   298             val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
   299             val session =
   299             val session = Session(session_name, threads, entry :: entries, ml_stats)
   300               sessions.get(session_name) match {
       
   301                 case None =>
       
   302                   Session(session_name, threads, List(entry), ml_stats, entry.date)
       
   303                 case Some(old) =>
       
   304                   val (ml_stats1, ml_stats1_date) =
       
   305                     if (entry.date > old.ml_statistics_date) (ml_stats, entry.date)
       
   306                     else (old.ml_statistics, old.ml_statistics_date)
       
   307                   Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
       
   308               }
   300 
   309 
   301             if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
   310             if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
   302               data_entries += (data_name -> (sessions + (session_name -> session)))
   311               data_entries += (data_name -> (sessions + (session_name -> session)))
   303             }
   312             }
   304           }
   313           }