src/Pure/Admin/build_stats.scala
changeset 65741 cf42659364c9
parent 65740 83388f09e9ab
child 65742 b9e0f25ba16a
equal deleted inserted replaced
65740:83388f09e9ab 65741:cf42659364c9
    89                 "_M" + threads.getOrElse(1)
    89                 "_M" + threads.getOrElse(1)
    90 
    90 
    91             val session = res.string(Build_Log.Data.session_name)
    91             val session = res.string(Build_Log.Data.session_name)
    92             val entry =
    92             val entry =
    93               Entry(res.date(Build_Log.Data.pull_date),
    93               Entry(res.date(Build_Log.Data.pull_date),
    94                 Timing(
    94                 res.timing(
    95                   Time.ms(res.long(Build_Log.Data.timing_elapsed)),
    95                   Build_Log.Data.timing_elapsed,
    96                   Time.ms(res.long(Build_Log.Data.timing_cpu)),
    96                   Build_Log.Data.timing_cpu,
    97                   Time.ms(res.long(Build_Log.Data.timing_gc))),
    97                   Build_Log.Data.timing_gc),
    98                 Timing(
    98                 res.timing(
    99                   Time.ms(res.long(Build_Log.Data.ml_timing_elapsed)),
    99                   Build_Log.Data.ml_timing_elapsed,
   100                   Time.ms(res.long(Build_Log.Data.ml_timing_cpu)),
   100                   Build_Log.Data.ml_timing_cpu,
   101                   Time.ms(res.long(Build_Log.Data.ml_timing_gc))))
   101                   Build_Log.Data.ml_timing_gc))
   102 
   102 
   103             val session_entries = data.getOrElse(name, Map.empty)
   103             val session_entries = data.getOrElse(name, Map.empty)
   104             val entries = session_entries.getOrElse(session, Nil)
   104             val entries = session_entries.getOrElse(session, Nil)
   105             data += (name -> (session_entries + (session -> (entry :: entries))))
   105             data += (name -> (session_entries + (session -> (entry :: entries))))
   106           }
   106           }