approximate repository identify job based on isabelle-nightly-slow;
more Jenkins changeset patterns found in the wild;

--- a/src/Pure/Admin/build_log.scala	Mon May 01 20:29:44 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 01 22:45:39 2017 +0200
@@ -311,7 +311,17 @@
   object Identify
   {
     val log_prefix = "isabelle_identify_"
-    val engine = "identify"
+
+    def engine(log_file: Log_File): String =
+      if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"
+      else "identify"
+
+    def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String =
+      terminate_lines(
+        List("isabelle_identify: " + Build_Log.print_date(date), "") :::
+        isabelle_version.map("Isabelle version: " + _).toList :::
+        afp_version.map("AFP version: " + _).toList)
+
     val Start = new Regex("""^isabelle_identify: (.+)$""")
     val No_End = new Regex("""$.""")
     val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
@@ -348,8 +358,10 @@
     val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""")
     val Start_Date = new Regex("""^Build started at (.+)$""")
     val No_End = new Regex("""$.""")
-    val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
-    val AFP_Version = new Regex("""^AFP id (\S+)$""")
+    val Isabelle_Version =
+      new Regex("""^(?:Build for Isabelle id |Isabelle id |ISABELLE_CI_REPO_ID=")(\w+).*$""")
+    val AFP_Version =
+      new Regex("""^(?:Build for AFP id |AFP id |ISABELLE_CI_AFP_ID=")(\w+).*$""")
     val CONFIGURATION = "=== CONFIGURATION ==="
     val BUILD = "=== BUILD ==="
   }
@@ -391,7 +403,7 @@
           log_file.get_all_settings)
 
       case Identify.Start(log_file.Strict_Date(start)) :: _ =>
-        parse(Identify.engine, "", start, Identify.No_End,
+        parse(Identify.engine(log_file), "", start, Identify.No_End,
           Identify.Isabelle_Version, Identify.AFP_Version)
 
       case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>

--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon May 01 20:29:44 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon May 01 22:45:39 2017 +0200
@@ -48,11 +48,7 @@
           val afp_rev = Mercurial.setup_repository(afp_source, afp_repos).id()
 
           File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
-            terminate_lines(
-              List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
-                "",
-                "Isabelle version: " + rev,
-                "AFP version: " + afp_rev)))
+            Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
 
           val new_snapshot = release_snapshot.ext("new")
           val old_snapshot = release_snapshot.ext("old")

--- a/src/Pure/Admin/jenkins.scala	Mon May 01 20:29:44 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 22:45:39 2017 +0200
@@ -52,6 +52,7 @@
 
   sealed case class Job_Info(
     job_name: String,
+    identify: Boolean,
     timestamp: Long,
     main_log: URL,
     session_logs: List[(String, String, URL)])
@@ -86,21 +87,32 @@
     def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
     {
       val log_dir = dir + Build_Log.log_subdir(date)
-      val log_path = log_dir + log_filename.ext("xz")
+      val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz"))
 
       if (!log_path.is_file) {
         progress.echo(log_path.expand.implode)
+        Isabelle_System.mkdirs(log_dir)
 
-        val ml_statistics =
-          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
-            read_ml_statistics(store, session_name).
-              map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
+        if (identify) {
+          val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log))
+          val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version)
+          val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version)
 
-        Isabelle_System.mkdirs(log_dir)
-        File.write_xz(log_path,
-          terminate_lines(Url.read(main_log) ::
-            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
-          XZ.options(6))
+          File.write(log_path,
+            Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" +
+              main_log.toString)
+        }
+        else {
+          val ml_statistics =
+            session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
+              read_ml_statistics(store, session_name).
+                map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
+
+          File.write_xz(log_path,
+            terminate_lines(Url.read(main_log) ::
+              ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
+            XZ.options(6))
+        }
       }
     }
   }
@@ -109,24 +121,30 @@
   {
     val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
 
+    val identify = job_name == "identify"
+    val job = if (identify) "isabelle-nightly-slow" else job_name
+
     val infos =
       for {
         build <-
           JSON.array(
-            invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
+            invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"),
             "allBuilds").getOrElse(Nil)
         number <- JSON.int(build, "number")
         timestamp <- JSON.long(build, "timestamp")
       } yield {
-        val job_prefix = root() + "/job/" + job_name + "/" + number
+        val job_prefix = root() + "/job/" + job + "/" + number
         val main_log = Url(job_prefix + "/consoleText")
         val session_logs =
-          for {
-            artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
-            log_path <- JSON.string(artifact, "relativePath")
-            (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
-          } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
-        Job_Info(job_name, timestamp, main_log, session_logs)
+          if (identify) Nil
+          else {
+            for {
+              artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
+              log_path <- JSON.string(artifact, "relativePath")
+              (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
+            } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
+          }
+        Job_Info(job_name, identify, timestamp, main_log, session_logs)
       }
 
     infos.sortBy(info => - info.timestamp)