clarified toString for toml objects;
authorFabian Huch <huch@in.tum.de>
Thu, 16 Nov 2023 15:19:24 +0100
changeset 78978 80fda74a045d
parent 78977 c7db5b4dbace
child 78979 d5ce982ae60f
clarified toString for toml objects;
src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Thu Nov 16 14:33:45 2023 +0100
+++ b/src/Pure/General/toml.scala	Thu Nov 16 15:19:24 2023 +0100
@@ -60,6 +60,7 @@
       case other: Array => rep == other.rep
       case _ => false
     }
+    override def toString: Str = "Array(" + length.toString + ")"
 
     class Values[A](pf: PartialFunction[T, A]) { def values: List[A] = rep.collect(pf).reverse }
     lazy val string = new Values({ case s: String => s })
@@ -93,6 +94,12 @@
         case other: Table => rep == other.rep
         case _ => false
       }
+    override def toString: Str =
+      rep.map {
+        case (k, t: Table) => k + "(" + t.domain.size + ")"
+        case (k, a: Array) => k + "(" + a.length + ")"
+        case (k, _) => k
+      }.mkString("Table(", ", ", ")")
 
     class Value[A: ClassTag](pf: PartialFunction[T, A]) {
       def values: List[(Key, A)] =