API for Isabelle Jenkins continuous integration services;

--- a/Admin/etc/settings	Tue Aug 09 23:19:35 2016 +0200
+++ b/Admin/etc/settings	Tue Aug 09 23:26:51 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/Tools/ci_api.scala	Tue Aug 09 23:26:51 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 23:19:35 2016 +0200
+++ b/src/Pure/build-jars	Tue Aug 09 23:26:51 2016 +0200
@@ -104,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