src/Pure/ML/ml_statistics.scala

   val fields: Set[String],
   val content: List[ML_Statistics.Entry],
   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 =
     content.foldLeft(0.0) { case (m, e) => m max e.get(field) }