simplified signature;
authorwenzelm
Thu, 18 May 2017 13:51:25 +0200
changeset 65864 1945fa8f0c39
parent 65863 94fe5e82d101
child 65865 177b90f33f40
simplified signature;
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)