--- 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()
}