tuned signature;
authorwenzelm
Fri Oct 27 17:04:41 2017 +0200 (19 months ago)
changeset 6692833f9133bed7c
parent 66927 153d7b68e8f8
child 66929 c19b17b72777
tuned signature;
src/Pure/General/json.scala
     1.1 --- a/src/Pure/General/json.scala	Fri Oct 27 16:21:58 2017 +0200
     1.2 +++ b/src/Pure/General/json.scala	Fri Oct 27 17:04:41 2017 +0200
     1.3 @@ -17,6 +17,9 @@
     1.4    type T = Any
     1.5    type S = String
     1.6  
     1.7 +  type Object = Map[String, T]
     1.8 +  val empty: Object = Map.empty
     1.9 +
    1.10  
    1.11    /* lexer */
    1.12  
    1.13 @@ -116,7 +119,7 @@
    1.14      def string: Parser[String] = elem("string", _.is_string) ^^ (_.text)
    1.15      def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble)
    1.16  
    1.17 -    def json_object: Parser[Map[String, T]] =
    1.18 +    def json_object: Parser[Object] =
    1.19        $$$("{") ~>
    1.20          repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~
    1.21        $$$("}") ^^ (_.toMap)
    1.22 @@ -184,7 +187,7 @@
    1.23          result += ']'
    1.24        }
    1.25  
    1.26 -      def object_(obj: Map[String, T])
    1.27 +      def object_(obj: Object)
    1.28        {
    1.29          result += '{'
    1.30          Library.separate(None, obj.toList.map(Some(_))).foreach({
    1.31 @@ -207,7 +210,7 @@
    1.32              result ++= (if (i.toDouble == n) i.toString else n.toString)
    1.33            case s: String => string(s)
    1.34            case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
    1.35 -            object_(obj.asInstanceOf[Map[String, T]])
    1.36 +            object_(obj.asInstanceOf[Object])
    1.37            case list: List[T] => array(list)
    1.38            case _ => error("Bad JSON value: " + x.toString)
    1.39          }
    1.40 @@ -257,9 +260,7 @@
    1.41  
    1.42    /* object values */
    1.43  
    1.44 -  val empty: Map[String, T] = Map.empty
    1.45 -
    1.46 -  def optional(entry: (String, Option[T])): Map[String, T] =
    1.47 +  def optional(entry: (String, Option[T])): Object =
    1.48      entry match {
    1.49        case (name, Some(x)) => Map(name -> x)
    1.50        case (_, None) => empty
    1.51 @@ -268,7 +269,7 @@
    1.52    def value(obj: T, name: String): Option[T] =
    1.53      obj match {
    1.54        case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
    1.55 -        m.asInstanceOf[Map[String, T]].get(name)
    1.56 +        m.asInstanceOf[Object].get(name)
    1.57        case _ => None
    1.58      }
    1.59