src/Pure/General/json.scala
changeset 64545 25045094d7bb
parent 63992 3aa9837d05c7
child 64761 ae97a5afffcc
     1.1 --- a/src/Pure/General/json.scala	Sun Oct 02 14:07:43 2016 +0200
     1.2 +++ b/src/Pure/General/json.scala	Sat Dec 10 17:20:39 2016 +0100
     1.3 @@ -7,48 +7,163 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.util.parsing.json.{JSONObject, JSONArray}
     1.8 +
     1.9  object JSON
    1.10  {
    1.11 -  /* parse */
    1.12 +  type T = Any
    1.13 +  type S = String
    1.14  
    1.15 -  def parse(text: String): Any =
    1.16 -    scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON")
    1.17  
    1.18 +  /* standard format */
    1.19  
    1.20 -  /* field access */
    1.21 +  def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON")
    1.22  
    1.23 -  def any(obj: Any, name: String): Option[Any] =
    1.24 +  object Format
    1.25 +  {
    1.26 +    def unapply(s: S): Option[T] =
    1.27 +      try { scala.util.parsing.json.JSON.parseFull(s) }
    1.28 +      catch { case ERROR(_) => None }
    1.29 +
    1.30 +    def apply(json: T): S =
    1.31 +    {
    1.32 +      val result = new StringBuilder
    1.33 +
    1.34 +      def string(s: String)
    1.35 +      {
    1.36 +        result += '"'
    1.37 +        result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
    1.38 +        result += '"'
    1.39 +      }
    1.40 +
    1.41 +      def array(list: List[T])
    1.42 +      {
    1.43 +        result += '['
    1.44 +        Library.separate(None, list.map(Some(_))).foreach({
    1.45 +          case None => result += ','
    1.46 +          case Some(x) => json_format(x)
    1.47 +        })
    1.48 +        result += ']'
    1.49 +      }
    1.50 +
    1.51 +      def object_(obj: Map[String, T])
    1.52 +      {
    1.53 +        result += '{'
    1.54 +        Library.separate(None, obj.toList.map(Some(_))).foreach({
    1.55 +          case None => result += ','
    1.56 +          case Some((x, y)) =>
    1.57 +            string(x)
    1.58 +            result += ':'
    1.59 +            json_format(y)
    1.60 +        })
    1.61 +        result += '}'
    1.62 +      }
    1.63 +
    1.64 +      def json_format(x: T)
    1.65 +      {
    1.66 +        x match {
    1.67 +          case null => result ++= "null"
    1.68 +          case _: Int | _: Long | _: Boolean => result ++= x.toString
    1.69 +          case n: Double =>
    1.70 +            val i = n.toLong
    1.71 +            result ++= (if (i.toDouble == n) i.toString else n.toString)
    1.72 +          case s: String => string(s)
    1.73 +          case JSONObject(obj) => object_(obj)
    1.74 +          case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
    1.75 +            object_(obj.asInstanceOf[Map[String, T]])
    1.76 +          case JSONArray(list) => array(list)
    1.77 +          case list: List[T] => array(list)
    1.78 +          case _ => error("Bad JSON value: " + x.toString)
    1.79 +        }
    1.80 +      }
    1.81 +
    1.82 +      json_format(json)
    1.83 +      result.toString
    1.84 +    }
    1.85 +  }
    1.86 +
    1.87 +
    1.88 +  /* numbers */
    1.89 +
    1.90 +  object Number
    1.91 +  {
    1.92 +    object Double {
    1.93 +      def unapply(json: T): Option[scala.Double] =
    1.94 +        json match {
    1.95 +          case x: scala.Double => Some(x)
    1.96 +          case x: scala.Long => Some(x.toDouble)
    1.97 +          case x: scala.Int => Some(x.toDouble)
    1.98 +          case _ => None
    1.99 +        }
   1.100 +    }
   1.101 +
   1.102 +    object Long {
   1.103 +      def unapply(json: T): Option[scala.Long] =
   1.104 +        json match {
   1.105 +          case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong)
   1.106 +          case x: scala.Long => Some(x)
   1.107 +          case x: scala.Int => Some(x.toLong)
   1.108 +          case _ => None
   1.109 +        }
   1.110 +    }
   1.111 +
   1.112 +    object Int {
   1.113 +      def unapply(json: T): Option[scala.Int] =
   1.114 +        json match {
   1.115 +          case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt)
   1.116 +          case x: scala.Long if x.toInt.toLong == x => Some(x.toInt)
   1.117 +          case x: scala.Int => Some(x)
   1.118 +          case _ => None
   1.119 +        }
   1.120 +    }
   1.121 +  }
   1.122 +
   1.123 +
   1.124 +  /* object values */
   1.125 +
   1.126 +  def value(obj: T, name: String): Option[T] =
   1.127      obj match {
   1.128 -      case m: Map[String, Any] => m.get(name)
   1.129 +      case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
   1.130 +        m.asInstanceOf[Map[String, T]].get(name)
   1.131        case _ => None
   1.132      }
   1.133  
   1.134 -  def array(obj: Any, name: String): List[Any] =
   1.135 -    any(obj, name) match {
   1.136 -      case Some(a: List[Any]) => a
   1.137 -      case _ => Nil
   1.138 +  def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] =
   1.139 +    for {
   1.140 +      json <- value(obj, name)
   1.141 +      x <- unapply(json)
   1.142 +    } yield x
   1.143 +
   1.144 +  def array(obj: T, name: String): Option[List[T]] =
   1.145 +    value(obj, name) match {
   1.146 +      case Some(a: List[T]) => Some(a)
   1.147 +      case _ => None
   1.148      }
   1.149  
   1.150 -  def string(obj: Any, name: String): Option[String] =
   1.151 -    any(obj, name) match {
   1.152 +  def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] =
   1.153 +    for {
   1.154 +      a0 <- array(obj, name)
   1.155 +      a = a0.map(unapply(_))
   1.156 +      if a.forall(_.isDefined)
   1.157 +    } yield a.map(_.get)
   1.158 +
   1.159 +  def string(obj: T, name: String): Option[String] =
   1.160 +    value(obj, name) match {
   1.161        case Some(x: String) => Some(x)
   1.162        case _ => None
   1.163      }
   1.164  
   1.165 -  def double(obj: Any, name: String): Option[Double] =
   1.166 -    any(obj, name) match {
   1.167 -      case Some(x: Double) => Some(x)
   1.168 -      case _ => None
   1.169 -    }
   1.170 +  def double(obj: T, name: String): Option[Double] =
   1.171 +    value(obj, name, Number.Double.unapply)
   1.172  
   1.173 -  def long(obj: Any, name: String): Option[Long] =
   1.174 -    double(obj, name).map(_.toLong)
   1.175 +  def long(obj: T, name: String): Option[Long] =
   1.176 +    value(obj, name, Number.Long.unapply)
   1.177  
   1.178 -  def int(obj: Any, name: String): Option[Int] =
   1.179 -    double(obj, name).map(_.toInt)
   1.180 +  def int(obj: T, name: String): Option[Int] =
   1.181 +    value(obj, name, Number.Int.unapply)
   1.182  
   1.183 -  def bool(obj: Any, name: String): Option[Boolean] =
   1.184 -    any(obj, name) match {
   1.185 +  def bool(obj: T, name: String): Option[Boolean] =
   1.186 +    value(obj, name) match {
   1.187        case Some(x: Boolean) => Some(x)
   1.188        case _ => None
   1.189      }