tuned output;
authorwenzelm
Sun, 12 Nov 2023 12:54:26 +0100
changeset 78959 78698a97afb3
parent 78958 c125f75a5144
child 78960 f4e7dec70fa4
tuned output;
src/Pure/System/registry.scala
--- a/src/Pure/System/registry.scala	Sun Nov 12 12:34:04 2023 +0100
+++ b/src/Pure/System/registry.scala	Sun Nov 12 12:54:26 2023 +0100
@@ -52,7 +52,16 @@
 }
 
 class Registry private(val table: TOML.Table) {
-  override def toString: String = TOML.Format(table)
+  override def toString: String =
+    (for (a <- table.domain.toList.sorted.iterator) yield {
+      val size =
+        table.any.get(a) match {
+          case Some(t: TOML.Array) => "(" + t.length + ")"
+          case Some(t: TOML.Table) => "(" + t.domain.size + ")"
+          case _ => ""
+        }
+      a + size
+    }).mkString("Registry(", ", ", ")")
 
   def get[A](category: Registry.Category[A], name: String): A = {
     table.any.get(category.prefix) match {