src/Pure/General/json.scala
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 {