tuned output;
authorwenzelm
Sat, 27 Nov 2021 14:03:44 +0100
changeset 75257 7420a7ac1a4c
parent 75256 204273f3a30e
child 75258 014141670774
tuned output;
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 =