# HG changeset patch
# User wenzelm
# Date 1509116681 -7200
# Node ID 33f9133bed7c38eacb01707ba026a3e8c856b3ac
# Parent  153d7b68e8f82465d2d04b0f9d4377753827d68d
tuned signature;

diff -r 153d7b68e8f8 -r 33f9133bed7c src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Fri Oct 27 16:21:58 2017 +0200
+++ b/src/Pure/General/json.scala	Fri Oct 27 17:04:41 2017 +0200
@@ -17,6 +17,9 @@
   type T = Any
   type S = String
 
+  type Object = Map[String, T]
+  val empty: Object = Map.empty
+
 
   /* lexer */
 
@@ -116,7 +119,7 @@
     def string: Parser[String] = elem("string", _.is_string) ^^ (_.text)
     def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble)
 
-    def json_object: Parser[Map[String, T]] =
+    def json_object: Parser[Object] =
       $$$("{") ~>
         repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~
       $$$("}") ^^ (_.toMap)
@@ -184,7 +187,7 @@
         result += ']'
       }
 
-      def object_(obj: Map[String, T])
+      def object_(obj: Object)
       {
         result += '{'
         Library.separate(None, obj.toList.map(Some(_))).foreach({
@@ -207,7 +210,7 @@
             result ++= (if (i.toDouble == n) i.toString else n.toString)
           case s: String => string(s)
           case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
-            object_(obj.asInstanceOf[Map[String, T]])
+            object_(obj.asInstanceOf[Object])
           case list: List[T] => array(list)
           case _ => error("Bad JSON value: " + x.toString)
         }
@@ -257,9 +260,7 @@
 
   /* object values */
 
-  val empty: Map[String, T] = Map.empty
-
-  def optional(entry: (String, Option[T])): Map[String, T] =
+  def optional(entry: (String, Option[T])): Object =
     entry match {
       case (name, Some(x)) => Map(name -> x)
       case (_, None) => empty
@@ -268,7 +269,7 @@
   def value(obj: T, name: String): Option[T] =
     obj match {
       case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
-        m.asInstanceOf[Map[String, T]].get(name)
+        m.asInstanceOf[Object].get(name)
       case _ => None
     }