src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Sat Jan 28 13:44:00 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Jan 28 15:04:15 2023 +0100
@@ -116,7 +116,7 @@
   def mem_scale(x: Long): Long = x / 1024 / 1024
 
   def mem_field_scale(name: String, x: Double): Double =
-    if (heap_fields._2.contains(name) || program_fields._2.contains(name)) {
+    if (heap_fields.names.contains(name) || program_fields.names.contains(name)) {
       mem_scale(x.toLong).toDouble
     }
     else x
@@ -128,43 +128,43 @@
 
   /* standard fields */
 
-  type Fields = (String, List[String])
+  sealed case class Fields(title: String, names: List[String])
 
   val tasks_fields: Fields =
-    ("Future tasks",
+    Fields("Future tasks",
       List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
         "tasks_urgent", "tasks_total"))
 
   val workers_fields: Fields =
-    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+    Fields("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
 
   val GC_fields: Fields =
-    ("GCs", List("partial_GCs", "full_GCs", "share_passes"))
+    Fields("GCs", List("partial_GCs", "full_GCs", "share_passes"))
 
   val heap_fields: Fields =
-    ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
+    Fields("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
       "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
 
   val program_fields: Fields =
-    ("Program", List("size_code", "size_stacks"))
+    Fields("Program", List("size_code", "size_stacks"))
 
   val threads_fields: Fields =
-    ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
+    Fields("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
 
   val time_fields: Fields =
-    ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
+    Fields("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
 
   val speed_fields: Fields =
-    ("Speed", List("speed_CPU", "speed_GC"))
+    Fields("Speed", List("speed_CPU", "speed_GC"))
 
   private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
 
   val java_heap_fields: Fields =
-    ("Java heap", List("java_heap_size", "java_heap_used"))
+    Fields("Java heap", List("java_heap_size", "java_heap_used"))
 
   val java_thread_fields: Fields =
-    ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active"))
+    Fields("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active"))
 
 
   val main_fields: List[Fields] =
@@ -299,7 +299,7 @@
   }
 
   def chart(fields: ML_Statistics.Fields): JFreeChart =
-    chart(fields._1, fields._2)
+    chart(fields.title, fields.names)
 
   def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
     fields.map(chart).foreach(c =>