# HG changeset patch
# User wenzelm
# Date 1699455922 -3600
# Node ID 7847cbfe3a62db22b6a5f383eafcc66c050961e5
# Parent  8378354bbdad5036d8d69e3326f6bbed73d12f7c
more operations;

diff -r 8378354bbdad -r 7847cbfe3a62 src/Pure/General/toml.scala
--- 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()
   }