--- a/src/Pure/General/json.scala Tue Mar 13 19:35:08 2018 +0100
+++ b/src/Pure/General/json.scala Tue Mar 13 20:02:09 2018 +0100
@@ -20,7 +20,9 @@
object Object
{
type T = Map[String, JSON.T]
- val empty: T = Map.empty
+ val empty: Object.T = Map.empty
+
+ def apply(entries: (String, JSON.T)*): Object.T = Map(entries:_*)
def unapply(obj: T): Option[Object.T] =
obj match {
@@ -299,7 +301,7 @@
def optional(entry: (String, Option[T])): Object.T =
entry match {
- case (name, Some(x)) => Map(name -> x)
+ case (name, Some(x)) => Object(name -> x)
case (_, None) => Object.empty
}