# HG changeset patch
# User wenzelm
# Date 1495108285 -7200
# Node ID 1945fa8f0c392f901a79cd32b8d7e97ec5fe3a86
# Parent  94fe5e82d1013cc9af5c153d6f27df1046374724
simplified signature;

diff -r 94fe5e82d101 -r 1945fa8f0c39 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Thu May 18 11:42:16 2017 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu May 18 13:51:25 2017 +0200
@@ -29,7 +29,7 @@
 
   val HEAP_SIZE = "size_heap"
 
-  type Fields = (String, Iterable[String])
+  type Fields = (String, List[String])
 
   val tasks_fields: Fields =
     ("Future tasks",
@@ -153,7 +153,7 @@
 
   /* charts */
 
-  def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
+  def update_data(data: XYSeriesCollection, selected_fields: List[String])
   {
     data.removeAllSeries
     for {
@@ -165,7 +165,7 @@
     }
   }
 
-  def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+  def chart(title: String, selected_fields: List[String]): JFreeChart =
   {
     val data = new XYSeriesCollection
     update_data(data, selected_fields)