# HG changeset patch # User wenzelm # Date 1699790066 -3600 # Node ID 78698a97afb36148e667432559b23e54ac2bf70c # Parent c125f75a51440a1f524090c0ddeccfc871954323 tuned output; diff -r c125f75a5144 -r 78698a97afb3 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 {