--- a/src/Pure/ML/ml_statistics.scala Thu Aug 13 12:33:44 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala Thu Aug 13 12:38:44 2020 +0200
@@ -173,12 +173,11 @@
private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
+ val main_fields: List[Fields] =
+ List(heap_fields, tasks_fields, workers_fields)
+
val all_fields: List[Fields] =
- List(tasks_fields, workers_fields, GC_fields, heap_fields, program_fields, threads_fields,
- time_fields, speed_fields)
-
- val main_fields: List[Fields] =
- List(tasks_fields, workers_fields, heap_fields)
+ main_fields ::: List(threads_fields, GC_fields, program_fields, time_fields, speed_fields)
/* content interpretation */