# HG changeset patch # User wenzelm # Date 1481386839 -3600 # Node ID 25045094d7bbe07b7a8eecd75aecf088d531e908 # Parent d23b7c9b9dd4c9184f7f774de316b4e4eae7e313 clarified JSON operations (see isabelle_vscode/a7931dc2a1ab); diff -r d23b7c9b9dd4 -r 25045094d7bb src/Pure/Admin/ci_api.scala --- a/src/Pure/Admin/ci_api.scala Sat Dec 10 15:45:16 2016 +0100 +++ b/src/Pure/Admin/ci_api.scala Sat Dec 10 17:20:39 2016 +0100 @@ -32,7 +32,7 @@ def build_jobs(): List[String] = for { - job <- JSON.array(invoke(root()), "jobs") + job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil) _class <- JSON.string(job, "_class") if _class == "hudson.model.FreeStyleProject" name <- JSON.string(job, "name") @@ -56,7 +56,8 @@ for { build <- JSON.array( - invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds") + invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds") + .getOrElse(Nil) number <- JSON.int(build, "number") timestamp <- JSON.long(build, "timestamp") } yield { @@ -64,7 +65,7 @@ val output = Url(job_prefix + "/consoleText") val session_logs = for { - artifact <- JSON.array(build, "artifacts") + artifact <- JSON.array(build, "artifacts").getOrElse(Nil) log_path <- JSON.string(artifact, "relativePath") session <- (log_path match { case Log_Session(name) => Some(name) case _ => None }) } yield (session -> Url(job_prefix + "/artifact/" + log_path)) diff -r d23b7c9b9dd4 -r 25045094d7bb src/Pure/General/json.scala --- a/src/Pure/General/json.scala Sat Dec 10 15:45:16 2016 +0100 +++ b/src/Pure/General/json.scala Sat Dec 10 17:20:39 2016 +0100 @@ -7,48 +7,163 @@ package isabelle +import scala.util.parsing.json.{JSONObject, JSONArray} + object JSON { - /* parse */ - - def parse(text: String): Any = - scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON") + type T = Any + type S = String - /* field access */ + /* standard format */ + + def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON") + + object Format + { + def unapply(s: S): Option[T] = + try { scala.util.parsing.json.JSON.parseFull(s) } + catch { case ERROR(_) => None } + + def apply(json: T): S = + { + val result = new StringBuilder + + def string(s: String) + { + result += '"' + result ++= scala.util.parsing.json.JSONFormat.quoteString(s) + result += '"' + } + + def array(list: List[T]) + { + result += '[' + Library.separate(None, list.map(Some(_))).foreach({ + case None => result += ',' + case Some(x) => json_format(x) + }) + result += ']' + } + + def object_(obj: Map[String, T]) + { + result += '{' + Library.separate(None, obj.toList.map(Some(_))).foreach({ + case None => result += ',' + case Some((x, y)) => + string(x) + result += ':' + json_format(y) + }) + result += '}' + } - def any(obj: Any, name: String): Option[Any] = + def json_format(x: T) + { + x match { + case null => result ++= "null" + case _: Int | _: Long | _: Boolean => result ++= x.toString + case n: Double => + val i = n.toLong + result ++= (if (i.toDouble == n) i.toString else n.toString) + case s: String => string(s) + case JSONObject(obj) => object_(obj) + case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) => + object_(obj.asInstanceOf[Map[String, T]]) + case JSONArray(list) => array(list) + case list: List[T] => array(list) + case _ => error("Bad JSON value: " + x.toString) + } + } + + json_format(json) + result.toString + } + } + + + /* numbers */ + + object Number + { + object Double { + def unapply(json: T): Option[scala.Double] = + json match { + case x: scala.Double => Some(x) + case x: scala.Long => Some(x.toDouble) + case x: scala.Int => Some(x.toDouble) + case _ => None + } + } + + object Long { + def unapply(json: T): Option[scala.Long] = + json match { + case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) + case x: scala.Long => Some(x) + case x: scala.Int => Some(x.toLong) + case _ => None + } + } + + object Int { + def unapply(json: T): Option[scala.Int] = + json match { + case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) + case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) + case x: scala.Int => Some(x) + case _ => None + } + } + } + + + /* object values */ + + def value(obj: T, name: String): Option[T] = obj match { - case m: Map[String, Any] => m.get(name) + case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => + m.asInstanceOf[Map[String, T]].get(name) case _ => None } - def array(obj: Any, name: String): List[Any] = - any(obj, name) match { - case Some(a: List[Any]) => a - case _ => Nil + def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] = + for { + json <- value(obj, name) + x <- unapply(json) + } yield x + + def array(obj: T, name: String): Option[List[T]] = + value(obj, name) match { + case Some(a: List[T]) => Some(a) + case _ => None } - def string(obj: Any, name: String): Option[String] = - any(obj, name) match { + def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = + for { + a0 <- array(obj, name) + a = a0.map(unapply(_)) + if a.forall(_.isDefined) + } yield a.map(_.get) + + def string(obj: T, name: String): Option[String] = + value(obj, name) match { case Some(x: String) => Some(x) case _ => None } - def double(obj: Any, name: String): Option[Double] = - any(obj, name) match { - case Some(x: Double) => Some(x) - case _ => None - } + def double(obj: T, name: String): Option[Double] = + value(obj, name, Number.Double.unapply) + + def long(obj: T, name: String): Option[Long] = + value(obj, name, Number.Long.unapply) - def long(obj: Any, name: String): Option[Long] = - double(obj, name).map(_.toLong) + def int(obj: T, name: String): Option[Int] = + value(obj, name, Number.Int.unapply) - def int(obj: Any, name: String): Option[Int] = - double(obj, name).map(_.toInt) - - def bool(obj: Any, name: String): Option[Boolean] = - any(obj, name) match { + def bool(obj: T, name: String): Option[Boolean] = + value(obj, name) match { case Some(x: Boolean) => Some(x) case _ => None }