clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
authorwenzelm
Sat Dec 10 17:20:39 2016 +0100 (18 months ago)
changeset 6454525045094d7bb
parent 64544 d23b7c9b9dd4
child 64546 134ae7da2ccf
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
src/Pure/Admin/ci_api.scala
src/Pure/General/json.scala
     1.1 --- a/src/Pure/Admin/ci_api.scala	Sat Dec 10 15:45:16 2016 +0100
     1.2 +++ b/src/Pure/Admin/ci_api.scala	Sat Dec 10 17:20:39 2016 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5    def build_jobs(): List[String] =
     1.6      for {
     1.7 -      job <- JSON.array(invoke(root()), "jobs")
     1.8 +      job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
     1.9        _class <- JSON.string(job, "_class")
    1.10        if _class == "hudson.model.FreeStyleProject"
    1.11        name <- JSON.string(job, "name")
    1.12 @@ -56,7 +56,8 @@
    1.13  
    1.14      for {
    1.15        build <- JSON.array(
    1.16 -        invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    1.17 +          invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    1.18 +        .getOrElse(Nil)
    1.19        number <- JSON.int(build, "number")
    1.20        timestamp <- JSON.long(build, "timestamp")
    1.21      } yield {
    1.22 @@ -64,7 +65,7 @@
    1.23        val output = Url(job_prefix + "/consoleText")
    1.24        val session_logs =
    1.25          for {
    1.26 -          artifact <- JSON.array(build, "artifacts")
    1.27 +          artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
    1.28            log_path <- JSON.string(artifact, "relativePath")
    1.29            session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
    1.30          } yield (session -> Url(job_prefix + "/artifact/" + log_path))
     2.1 --- a/src/Pure/General/json.scala	Sat Dec 10 15:45:16 2016 +0100
     2.2 +++ b/src/Pure/General/json.scala	Sat Dec 10 17:20:39 2016 +0100
     2.3 @@ -7,48 +7,163 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.util.parsing.json.{JSONObject, JSONArray}
     2.8 +
     2.9  object JSON
    2.10  {
    2.11 -  /* parse */
    2.12 +  type T = Any
    2.13 +  type S = String
    2.14  
    2.15 -  def parse(text: String): Any =
    2.16 -    scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON")
    2.17  
    2.18 +  /* standard format */
    2.19  
    2.20 -  /* field access */
    2.21 +  def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON")
    2.22  
    2.23 -  def any(obj: Any, name: String): Option[Any] =
    2.24 +  object Format
    2.25 +  {
    2.26 +    def unapply(s: S): Option[T] =
    2.27 +      try { scala.util.parsing.json.JSON.parseFull(s) }
    2.28 +      catch { case ERROR(_) => None }
    2.29 +
    2.30 +    def apply(json: T): S =
    2.31 +    {
    2.32 +      val result = new StringBuilder
    2.33 +
    2.34 +      def string(s: String)
    2.35 +      {
    2.36 +        result += '"'
    2.37 +        result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
    2.38 +        result += '"'
    2.39 +      }
    2.40 +
    2.41 +      def array(list: List[T])
    2.42 +      {
    2.43 +        result += '['
    2.44 +        Library.separate(None, list.map(Some(_))).foreach({
    2.45 +          case None => result += ','
    2.46 +          case Some(x) => json_format(x)
    2.47 +        })
    2.48 +        result += ']'
    2.49 +      }
    2.50 +
    2.51 +      def object_(obj: Map[String, T])
    2.52 +      {
    2.53 +        result += '{'
    2.54 +        Library.separate(None, obj.toList.map(Some(_))).foreach({
    2.55 +          case None => result += ','
    2.56 +          case Some((x, y)) =>
    2.57 +            string(x)
    2.58 +            result += ':'
    2.59 +            json_format(y)
    2.60 +        })
    2.61 +        result += '}'
    2.62 +      }
    2.63 +
    2.64 +      def json_format(x: T)
    2.65 +      {
    2.66 +        x match {
    2.67 +          case null => result ++= "null"
    2.68 +          case _: Int | _: Long | _: Boolean => result ++= x.toString
    2.69 +          case n: Double =>
    2.70 +            val i = n.toLong
    2.71 +            result ++= (if (i.toDouble == n) i.toString else n.toString)
    2.72 +          case s: String => string(s)
    2.73 +          case JSONObject(obj) => object_(obj)
    2.74 +          case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
    2.75 +            object_(obj.asInstanceOf[Map[String, T]])
    2.76 +          case JSONArray(list) => array(list)
    2.77 +          case list: List[T] => array(list)
    2.78 +          case _ => error("Bad JSON value: " + x.toString)
    2.79 +        }
    2.80 +      }
    2.81 +
    2.82 +      json_format(json)
    2.83 +      result.toString
    2.84 +    }
    2.85 +  }
    2.86 +
    2.87 +
    2.88 +  /* numbers */
    2.89 +
    2.90 +  object Number
    2.91 +  {
    2.92 +    object Double {
    2.93 +      def unapply(json: T): Option[scala.Double] =
    2.94 +        json match {
    2.95 +          case x: scala.Double => Some(x)
    2.96 +          case x: scala.Long => Some(x.toDouble)
    2.97 +          case x: scala.Int => Some(x.toDouble)
    2.98 +          case _ => None
    2.99 +        }
   2.100 +    }
   2.101 +
   2.102 +    object Long {
   2.103 +      def unapply(json: T): Option[scala.Long] =
   2.104 +        json match {
   2.105 +          case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong)
   2.106 +          case x: scala.Long => Some(x)
   2.107 +          case x: scala.Int => Some(x.toLong)
   2.108 +          case _ => None
   2.109 +        }
   2.110 +    }
   2.111 +
   2.112 +    object Int {
   2.113 +      def unapply(json: T): Option[scala.Int] =
   2.114 +        json match {
   2.115 +          case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt)
   2.116 +          case x: scala.Long if x.toInt.toLong == x => Some(x.toInt)
   2.117 +          case x: scala.Int => Some(x)
   2.118 +          case _ => None
   2.119 +        }
   2.120 +    }
   2.121 +  }
   2.122 +
   2.123 +
   2.124 +  /* object values */
   2.125 +
   2.126 +  def value(obj: T, name: String): Option[T] =
   2.127      obj match {
   2.128 -      case m: Map[String, Any] => m.get(name)
   2.129 +      case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
   2.130 +        m.asInstanceOf[Map[String, T]].get(name)
   2.131        case _ => None
   2.132      }
   2.133  
   2.134 -  def array(obj: Any, name: String): List[Any] =
   2.135 -    any(obj, name) match {
   2.136 -      case Some(a: List[Any]) => a
   2.137 -      case _ => Nil
   2.138 +  def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] =
   2.139 +    for {
   2.140 +      json <- value(obj, name)
   2.141 +      x <- unapply(json)
   2.142 +    } yield x
   2.143 +
   2.144 +  def array(obj: T, name: String): Option[List[T]] =
   2.145 +    value(obj, name) match {
   2.146 +      case Some(a: List[T]) => Some(a)
   2.147 +      case _ => None
   2.148      }
   2.149  
   2.150 -  def string(obj: Any, name: String): Option[String] =
   2.151 -    any(obj, name) match {
   2.152 +  def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] =
   2.153 +    for {
   2.154 +      a0 <- array(obj, name)
   2.155 +      a = a0.map(unapply(_))
   2.156 +      if a.forall(_.isDefined)
   2.157 +    } yield a.map(_.get)
   2.158 +
   2.159 +  def string(obj: T, name: String): Option[String] =
   2.160 +    value(obj, name) match {
   2.161        case Some(x: String) => Some(x)
   2.162        case _ => None
   2.163      }
   2.164  
   2.165 -  def double(obj: Any, name: String): Option[Double] =
   2.166 -    any(obj, name) match {
   2.167 -      case Some(x: Double) => Some(x)
   2.168 -      case _ => None
   2.169 -    }
   2.170 +  def double(obj: T, name: String): Option[Double] =
   2.171 +    value(obj, name, Number.Double.unapply)
   2.172  
   2.173 -  def long(obj: Any, name: String): Option[Long] =
   2.174 -    double(obj, name).map(_.toLong)
   2.175 +  def long(obj: T, name: String): Option[Long] =
   2.176 +    value(obj, name, Number.Long.unapply)
   2.177  
   2.178 -  def int(obj: Any, name: String): Option[Int] =
   2.179 -    double(obj, name).map(_.toInt)
   2.180 +  def int(obj: T, name: String): Option[Int] =
   2.181 +    value(obj, name, Number.Int.unapply)
   2.182  
   2.183 -  def bool(obj: Any, name: String): Option[Boolean] =
   2.184 -    any(obj, name) match {
   2.185 +  def bool(obj: T, name: String): Option[Boolean] =
   2.186 +    value(obj, name) match {
   2.187        case Some(x: Boolean) => Some(x)
   2.188        case _ => None
   2.189      }