more operations;
authorwenzelm
Wed, 08 Nov 2023 16:05:22 +0100
changeset 78919 7847cbfe3a62
parent 78918 8378354bbdad
child 78920 e495f910dd94
child 78922 9e43ab263d33
more operations;
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()
   }