src/Pure/Admin/build_status.scala
changeset 65861 f35abc25d7b1
parent 65860 ce6be2e40d47
child 65863 94fe5e82d101
equal deleted inserted replaced
65860:ce6be2e40d47 65861:f35abc25d7b1
    96     afp_version: String,
    96     afp_version: String,
    97     timing: Timing,
    97     timing: Timing,
    98     ml_timing: Timing,
    98     ml_timing: Timing,
    99     maximum_heap: Long,
    99     maximum_heap: Long,
   100     average_heap: Long,
   100     average_heap: Long,
   101     final_heap: Long,
   101     final_heap: Long)
   102     ml_statistics: ML_Statistics)
       
   103 
   102 
   104   def read_data(options: Options,
   103   def read_data(options: Options,
   105     progress: Progress = No_Progress,
   104     progress: Progress = No_Progress,
   106     profiles: List[Profile] = default_profiles,
   105     profiles: List[Profile] = default_profiles,
   107     only_sessions: Set[String] = Set.empty,
   106     only_sessions: Set[String] = Set.empty,
   195                     Build_Log.Data.ml_timing_elapsed,
   194                     Build_Log.Data.ml_timing_elapsed,
   196                     Build_Log.Data.ml_timing_cpu,
   195                     Build_Log.Data.ml_timing_cpu,
   197                     Build_Log.Data.ml_timing_gc),
   196                     Build_Log.Data.ml_timing_gc),
   198                 maximum_heap = ml_stats.maximum_heap_size,
   197                 maximum_heap = ml_stats.maximum_heap_size,
   199                 average_heap = ml_stats.average_heap_size,
   198                 average_heap = ml_stats.average_heap_size,
   200                 final_heap = res.long(Build_Log.Data.heap_size),
   199                 final_heap = res.long(Build_Log.Data.heap_size))
   201                 ml_statistics = ml_stats)
       
   202 
   200 
   203             val sessions = data_entries.getOrElse(data_name, Map.empty)
   201             val sessions = data_entries.getOrElse(data_name, Map.empty)
   204             val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
   202             val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
   205             val session = Session(session_name, threads, entry :: entries)
   203             val session = Session(session_name, threads, entry :: entries)
   206             data_entries += (data_name -> (sessions + (session_name -> session)))
   204             data_entries += (data_name -> (sessions + (session_name -> session)))