src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Mon May 17 14:07:51 2021 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Mon May 17 14:54:03 2021 +0200
@@ -58,12 +58,7 @@
   {
     def progress_stdout(line: String): Unit =
     {
-      val props =
-        Library.space_explode(',', line).flatMap((entry: String) =>
-          Library.space_explode('=', entry) match {
-            case List(a, b) => Some((a, b))
-            case _ => None
-          })
+      val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
       if (props.nonEmpty) consume(props)
     }