# HG changeset patch
# User wenzelm
# Date 1674914655 -3600
# Node ID 9a22256b0a274b059326586e748c0c9b395eca53
# Parent  00d1db8e496e6bb8a4d6f5a16542bae883744619
clarified signature: more explicit types;

diff -r 00d1db8e496e -r 9a22256b0a27 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Jan 28 13:44:00 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Jan 28 15:04:15 2023 +0100
@@ -502,7 +502,7 @@
                 val image = Image(plot_name, image_width, image_height)
                 val chart =
                   session.ml_statistics.chart(
-                    fields._1 + ": " + session.ml_statistics.heading, fields._2)
+                    fields.title + ": " + session.ml_statistics.heading, fields.names)
                 Graphics_File.write_chart_png(
                   (dir + image.path).file, chart, image.width, image.height)
                 image
diff -r 00d1db8e496e -r 9a22256b0a27 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 =>
diff -r 00d1db8e496e -r 9a22256b0a27 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Sat Jan 28 13:44:00 2023 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sat Jan 28 15:04:15 2023 +0100
@@ -44,14 +44,14 @@
     statistics_length = 0
   }
 
-  private var data_name = ML_Statistics.all_fields.head._1
+  private var data_name = ML_Statistics.all_fields.head.title
   private val chart = ML_Statistics.empty.chart(null, Nil)
   private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
 
   private def update_chart(): Unit = {
-    ML_Statistics.all_fields.find(_._1 == data_name) match {
+    ML_Statistics.all_fields.find(_.title == data_name) match {
       case None =>
-      case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields)
+      case Some(fields) => ML_Statistics(statistics.toList).update_data(data, fields.names)
     }
   }