diff -r 9efdebe24c65 -r 0ffcad1f6130 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -54,9 +54,9 @@
   def monitor(pid: Long,
     stats_dir: String = "",
     delay: Time = Time.seconds(0.5),
-    consume: Properties.T => Unit = Console.println)
+    consume: Properties.T => Unit = Console.println): Unit =
   {
-    def progress_stdout(line: String)
+    def progress_stdout(line: String): Unit =
     {
       val props =
         Library.space_explode(',', line).flatMap((entry: String) =>
@@ -289,7 +289,7 @@
 
   /* charts */
 
-  def update_data(data: XYSeriesCollection, selected_fields: List[String])
+  def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
   {
     data.removeAllSeries
     for (field <- selected_fields) {