# HG changeset patch
# User wenzelm
# Date 1597315124 -7200
# Node ID 4a46650bf701572ca487dd0417eb64b10c8c87a1
# Parent  6e8b5cdd4ba0a13f62537d7ffc004b0b1f8de534
clarified order for GUI;

diff -r 6e8b5cdd4ba0 -r 4a46650bf701 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 */