src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Fri Nov 26 19:44:21 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Nov 27 13:55:03 2021 +0100
@@ -194,7 +194,7 @@
   val empty: ML_Statistics = apply(Nil)
 
   def apply(ml_statistics0: List[Properties.T], heading: String = "",
-    domain: String => Boolean = (key: String) => true): ML_Statistics =
+    domain: String => Boolean = _ => true): ML_Statistics =
   {
     require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
 
@@ -286,7 +286,7 @@
 
   def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
   {
-    data.removeAllSeries
+    data.removeAllSeries()
     for (field <- selected_fields) {
       val series = new XYSeries(field)
       content.foreach(entry => series.add(entry.time, entry.get(field)))