clarified order for GUI;
authorwenzelm
Thu, 13 Aug 2020 12:38:44 +0200
changeset 72373 4a46650bf701
parent 72372 6e8b5cdd4ba0
child 72374 6a4e51ca53c3
clarified order for GUI;
src/Pure/ML/ml_statistics.scala
--- 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 */