src/Pure/Tools/ml_statistics.scala
changeset 53189 ee8b8dafef0e
parent 52888 671421cef590
child 57612 990ffb84489b
equal deleted inserted replaced
53188:bb5433b13ff2 53189:ee8b8dafef0e
    46   val time_fields = ("Time", List("time_CPU", "time_GC"))
    46   val time_fields = ("Time", List("time_CPU", "time_GC"))
    47 
    47 
    48   val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
    48   val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
    49 
    49 
    50   val tasks_fields =
    50   val tasks_fields =
    51     ("Future tasks",
    51     ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    52       List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
       
    53 
    52 
    54   val workers_fields =
    53   val workers_fields =
    55     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    54     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    56 
    55 
    57   val standard_fields =
    56   val standard_fields =