| changeset 67857 | 262d62a4c32b |
| parent 67850 | 3e9fe7a84b5d |
| child 67864 | 449ed1afa056 |
--- a/src/Pure/General/json.scala Wed Mar 14 16:48:05 2018 +0100 +++ b/src/Pure/General/json.scala Wed Mar 14 16:52:16 2018 +0100 @@ -19,10 +19,12 @@ object Object { + type Entry = (String, JSON.T) + type T = Map[String, JSON.T] val empty: Object.T = Map.empty - def apply(entries: (String, JSON.T)*): Object.T = Map(entries:_*) + def apply(entries: Entry*): Object.T = Map(entries:_*) def unapply(obj: T): Option[Object.T] = obj match {