src/Pure/General/toml.scala
changeset 78919 7847cbfe3a62
parent 78917 30e0c15a71f7
child 78920 e495f910dd94
--- a/src/Pure/General/toml.scala	Wed Nov 08 15:37:15 2023 +0100
+++ b/src/Pure/General/toml.scala	Wed Nov 08 16:05:22 2023 +0100
@@ -68,6 +68,7 @@
   object Array {
     def apply(elems: Iterable[T]): Array = new Array(elems.toList.reverse)
     def apply(elems: T*): Array = Array(elems)
+    val empty: Array = apply()
   }
 
   class Table private(private val rep: Map[Key, T]) extends T {
@@ -128,6 +129,7 @@
   object Table {
     def apply(elems: Iterable[(Key, T)]): Table = elems.foldLeft(new Table(ListMap.empty))(_ + _)
     def apply(elems: (Key, T)*): Table = Table(elems)
+    val empty: Table = apply()
   }