# HG changeset patch
# User wenzelm
# Date 1520876010 -3600
# Node ID 8ada8f6d9495f3f1a63dfd02efbc002a9c60c7d9
# Parent  a9d450fc5a4908ad871d2e57faea1e322bcc75b2
clarified signature;

diff -r a9d450fc5a49 -r 8ada8f6d9495 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Mon Mar 12 16:39:58 2018 +0100
+++ b/src/Pure/General/json.scala	Mon Mar 12 18:33:30 2018 +0100
@@ -17,8 +17,18 @@
   type T = Any
   type S = String
 
-  type Object = Map[String, T]
-  val empty: Object = Map.empty
+  object Object
+  {
+    type T = Map[String, JSON.T]
+    val empty: T = Map.empty
+
+    def unapply(obj: T): Option[Object.T] =
+      obj match {
+        case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
+          Some(m.asInstanceOf[Object.T])
+        case _ => None
+      }
+  }
 
 
   /* lexer */
@@ -120,7 +130,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[Object] =
+    def json_object: Parser[Object.T] =
       $$$("{") ~>
         repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~
       $$$("}") ^^ (_.toMap)
@@ -188,7 +198,7 @@
         result += ']'
       }
 
-      def object_(obj: Object)
+      def object_(obj: Object.T)
       {
         result += '{'
         Library.separate(None, obj.toList.map(Some(_))).foreach({
@@ -210,8 +220,7 @@
             val i = n.toLong
             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[Object])
+          case Object(m) => object_(m)
           case list: List[T] => array(list)
           case _ => error("Bad JSON value: " + x.toString)
         }
@@ -261,16 +270,15 @@
 
   /* object values */
 
-  def optional(entry: (String, Option[T])): Object =
+  def optional(entry: (String, Option[T])): Object.T =
     entry match {
       case (name, Some(x)) => Map(name -> x)
-      case (_, None) => empty
+      case (_, None) => Object.empty
     }
 
   def value(obj: T, name: String): Option[T] =
     obj match {
-      case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
-        m.asInstanceOf[Object].get(name)
+      case Object(m) => m.get(name)
       case _ => None
     }