# HG changeset patch
# User wenzelm
# Date 1638017703 -3600
# Node ID 204273f3a30ec9cb435552753814486946ab2c89
# Parent  5280c02f29dccf0a640f5f7e87b2275c34cea001
tuned;

diff -r 5280c02f29dc -r 204273f3a30e src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Fri Nov 26 19:44:21 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 27 13:55:03 2021 +0100
@@ -204,7 +204,7 @@
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     ml_statistics: Boolean = false,
-    ml_statistics_domain: String => Boolean = (key: String) => true,
+    ml_statistics_domain: String => Boolean = _ => true,
     verbose: Boolean = false): Data =
   {
     val date = Date.now()
@@ -377,7 +377,7 @@
           List(HTML.description(
             List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
         HTML.par(
-          List(HTML.itemize(data.entries.map({ case data_entry =>
+          List(HTML.itemize(data.entries.map(data_entry =>
             List(
               HTML.link(clean_name(data_entry.name) + "/index.html",
                 HTML.text(data_entry.name))) :::
@@ -388,7 +388,7 @@
                 List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
                 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
             })
-          }))))))
+          ))))))
 
     for (data_entry <- data.entries) {
       val data_name = data_entry.name
@@ -608,7 +608,7 @@
         "l:" -> (arg => options = options + ("build_log_history=" + arg)),
         "o:" -> (arg => options = options + arg),
         "s:" -> (arg =>
-          space_explode('x', arg).map(Value.Int.parse(_)) match {
+          space_explode('x', arg).map(Value.Int.parse) match {
             case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
             case _ => error("Error bad PNG image size: " + quote(arg))
           }),
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)))