merged

--- a/Admin/etc/settings	Tue Aug 09 21:18:32 2016 +0200
+++ b/Admin/etc/settings	Tue Aug 09 23:29:54 2016 +0200
@@ -1,3 +1,5 @@
 # -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+
+ISABELLE_JENKINS_ROOT="https://ci.isabelle.systems/jenkins"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/json.scala	Tue Aug 09 23:29:54 2016 +0200
@@ -0,0 +1,55 @@
+/*  Title:      Pure/Tools/json.scala
+    Author:     Makarius
+
+Support for JSON parsing.
+*/
+
+package isabelle
+
+
+object JSON
+{
+  /* parse */
+
+  def parse(text: String): Any =
+    scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON")
+
+
+  /* field access */
+
+  def any(obj: Any, name: String): Option[Any] =
+    obj match {
+      case m: Map[String, Any] => m.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 string(obj: Any, name: String): Option[String] =
+    any(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 long(obj: Any, name: String): Option[Long] =
+    double(obj, name).map(_.toLong)
+
+  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 {
+      case Some(x: Boolean) => Some(x)
+      case _ => None
+    }
+}

--- a/src/Pure/General/url.scala	Tue Aug 09 21:18:32 2016 +0200
+++ b/src/Pure/General/url.scala	Tue Aug 09 23:29:54 2016 +0200
@@ -33,13 +33,16 @@
 
   /* read */
 
-  private def gen_read(name: String, gzip: Boolean): String =
+  private def read(url: URL, gzip: Boolean): String =
   {
-    val stream = Url(name).openStream
+    val stream = url.openStream
     try { File.read_stream(if (gzip) new GZIPInputStream(stream) else stream) }
     finally { stream.close }
   }
 
-  def read(name: String): String = gen_read(name, false)
-  def read_gzip(name: String): String = gen_read(name, true)
+  def read(url: URL): String = read(url, false)
+  def read_gzip(url: URL): String = read(url, true)
+
+  def read(name: String): String = read(Url(name), false)
+  def read_gzip(name: String): String = read(Url(name), true)
 }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ci_api.scala	Tue Aug 09 23:29:54 2016 +0200
@@ -0,0 +1,74 @@
+/*  Title:      Pure/Tools/build.scala
+    Author:     Makarius
+
+API for Isabelle Jenkins continuous integration services.
+*/
+
+package isabelle
+
+
+import java.net.URL
+
+import scala.util.matching.Regex
+
+
+object CI_API
+{
+  /* CI service */
+
+  def root(): String =
+    Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
+
+  def invoke(url: String, args: String*): Any =
+  {
+    val req = url + "/api/json?" + args.mkString("&")
+    val result = Url.read(req)
+    try { JSON.parse(result) }
+    catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
+  }
+
+
+  /* build jobs */
+
+  def build_jobs(): List[String] =
+    for {
+      job <- JSON.array(invoke(root()), "jobs")
+      _class <- JSON.string(job, "_class")
+      if _class == "hudson.model.FreeStyleProject"
+      name <- JSON.string(job, "name")
+    } yield name
+
+  sealed case class Build_Info(
+    job_name: String,
+    timestamp: Long,
+    output: URL,
+    session_logs: List[(String, URL)])
+  {
+    def read_output(): String = Url.read(output)
+    def read_log(full_stats: Boolean, name: String): Build.Log_Info =
+      Build.parse_log(full_stats,
+        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
+  }
+
+  def build_job_builds(job_name: String): List[Build_Info] =
+  {
+    val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
+
+    for {
+      build <- JSON.array(
+        invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
+      number <- JSON.int(build, "number")
+      timestamp <- JSON.long(build, "timestamp")
+    } yield {
+      val job_prefix = root() + "/job/" + job_name + "/" + number
+      val output = Url(job_prefix + "/consoleText")
+      val session_logs =
+        for {
+          artifact <- JSON.array(build, "artifacts")
+          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))
+      Build_Info(job_name, timestamp, output, session_logs)
+    }
+  }
+}

--- a/src/Pure/build-jars	Tue Aug 09 21:18:32 2016 +0200
+++ b/src/Pure/build-jars	Tue Aug 09 23:29:54 2016 +0200
@@ -32,6 +32,7 @@
   General/graph.scala
   General/graph_display.scala
   General/graphics_file.scala
+  General/json.scala
   General/linear_set.scala
   General/long_name.scala
   General/multi_map.scala
@@ -103,6 +104,7 @@
   Tools/build_doc.scala
   Tools/check_keywords.scala
   Tools/check_sources.scala
+  Tools/ci_api.scala
   Tools/ci_profile.scala
   Tools/debugger.scala
   Tools/doc.scala