# HG changeset patch
# User wenzelm
# Date 1638018224 -3600
# Node ID 7420a7ac1a4cfb857bcccbbaab531681a9d230bb
# Parent  204273f3a30ec9cb435552753814486946ab2c89
tuned output;

diff -r 204273f3a30e -r 7420a7ac1a4c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Nov 27 13:55:03 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Nov 27 14:03:44 2021 +0100
@@ -260,6 +260,11 @@
   val time_start: Double,
   val duration: Double)
 {
+  override def toString: String =
+    if (content.isEmpty) "ML_Statistics.empty"
+    else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
   /* content */
 
   def maximum(field: String): Double =