diff -r 5280c02f29dc -r 204273f3a30e 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)))