author | wenzelm |
Sat, 27 Nov 2021 14:03:44 +0100 | |
changeset 74853 | 7420a7ac1a4c |
parent 74852 | 204273f3a30e |
child 74854 | 014141670774 |
--- 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 =