# HG changeset patch
# User wenzelm
# Date 1475940172 -7200
# Node ID c0b96b34c7b9f55cb047687cd778e55bc60f5734
# Parent  d54aa68e33dc00340016e4e9424e0849099a2b6e
support for Isabelle/Jenkins log file format;

diff -r d54aa68e33dc -r c0b96b34c7b9 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Sat Oct 08 16:07:41 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 17:22:52 2016 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/build_log.scala
     Author:     Makarius
 
-Build log parsing for current and historic versions.
+Build log parsing for current and historic formats.
 */
 
 package isabelle
@@ -9,7 +9,7 @@
 
 import java.io.{File => JFile}
 import java.time.ZoneId
-import java.time.format.DateTimeParseException
+import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.util.Locale
 
 import scala.collection.mutable
@@ -90,13 +90,18 @@
 
     def apply(path: Path): Log_File = apply(path.file)
 
+
+    /* date format */
+
     val Date_Format =
     {
       val fmts =
         Date.Formatter.variants(
           List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
           List(Locale.ENGLISH, Locale.GERMAN)) :::
-        List(Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
+        List(
+          DateTimeFormatter.RFC_1123_DATE_TIME,
+          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
 
       def tune_timezone(s: String): String =
         s match {
@@ -249,6 +254,19 @@
     val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
   }
 
+  object Jenkins
+  {
+    val engine = "jenkins"
+    val Start = new Regex("""^Started .*$""")
+    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 CONFIGURATION = "=== CONFIGURATION ==="
+    val BUILD = "=== BUILD ==="
+    val FINISHED = "Finished: "
+  }
+
   private def parse_meta_info(log_file: Log_File): Meta_Info =
   {
     def parse(engine: String, host: String, start: Date,
@@ -288,12 +306,22 @@
         parse(AFP_Test.engine, "", start, AFP_Test.End,
           AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
+      case Jenkins.Start() :: _
+      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
+         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
+        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
+          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
+            parse(Jenkins.engine, "", start, Jenkins.No_End,
+              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
+          case _ => Meta_Info.empty
+        }
+
       case line :: _ if line.startsWith("\0") => Meta_Info.empty
       case List(Isatest.End(_)) => Meta_Info.empty
       case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
       case Nil => Meta_Info.empty
 
-      case _ => log_file.err("cannot detect log header format")
+      case _ => log_file.err("cannot detect log file format")
     }
   }