--- 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) {