992 val session_entry = |
992 val session_entry = |
993 Session_Entry( |
993 Session_Entry( |
994 chapter = res.string(Data.chapter), |
994 chapter = res.string(Data.chapter), |
995 groups = split_lines(res.string(Data.groups)), |
995 groups = split_lines(res.string(Data.groups)), |
996 threads = res.get_int(Data.threads), |
996 threads = res.get_int(Data.threads), |
997 timing = |
997 timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc), |
998 Timing( |
|
999 Time.ms(res.long(Data.timing_elapsed)), |
|
1000 Time.ms(res.long(Data.timing_cpu)), |
|
1001 Time.ms(res.long(Data.timing_gc))), |
|
1002 ml_timing = |
998 ml_timing = |
1003 Timing( |
999 res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc), |
1004 Time.ms(res.long(Data.ml_timing_elapsed)), |
|
1005 Time.ms(res.long(Data.ml_timing_cpu)), |
|
1006 Time.ms(res.long(Data.ml_timing_gc))), |
|
1007 heap_size = res.get_long(Data.heap_size), |
1000 heap_size = res.get_long(Data.heap_size), |
1008 status = res.get_string(Data.status).map(Session_Status.withName(_)), |
1001 status = res.get_string(Data.status).map(Session_Status.withName(_)), |
1009 ml_statistics = |
1002 ml_statistics = |
1010 if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics)) |
1003 if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics)) |
1011 else Nil) |
1004 else Nil) |