--- 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))
--- 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
}