# HG changeset patch
# User wenzelm
# Date 1475922020 -7200
# Node ID 976289c733e6a1df9a1e03e88522ca575d19f7d9
# Parent  9b1573213ebe6fd2baf2fd34f8253e3356891a5d
more formal directory content;
clarified date format;

diff -r 9b1573213ebe -r 976289c733e6 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Sat Oct 08 11:21:29 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 12:20:20 2016 +0200
@@ -18,6 +18,19 @@
 
 object Build_Log
 {
+  /** directory content **/
+
+  def is_log(file: JFile): Boolean =
+    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
+
+  def isatest_files(dir: Path): List[JFile] =
+    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
+
+  def afp_test_files(dir: Path): List[JFile] =
+    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
+
+
+
   /** settings **/
 
   object Settings
@@ -90,6 +103,35 @@
       error("Error in log file " + quote(name) + ": " + msg)
 
 
+    /* date format */
+
+    val Date_Format =
+    {
+      val fmts =
+        Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")) ::
+        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))
+
+      // workaround undetected timezones
+      def tune(s: String): String =
+        Word.implode(Word.explode(s).map({
+          case "CET" | "MET" => "GMT+1"
+          case "CEST" | "MEST" => "GMT+2"
+          case "EST" => "GMT+1"  // FIXME ??
+          case a => a }))
+
+      Date.Format.make(fmts, tune)
+    }
+
+    object Strict_Date
+    {
+      def unapply(s: String): Some[Date] =
+        try { Some(Date_Format.parse(s)) }
+        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
+    }
+
+
     /* inlined content */
 
     def find[A](f: String => Option[A]): Option[A] =
@@ -166,24 +208,6 @@
 
   sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
 
-  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))
-
-    // workaround undetected timezones
-    def tune(s: String): String =
-      Word.implode(Word.explode(s).map({
-        case "CET" | "MET" => "GMT+1"
-        case "CEST" | "MEST" => "GMT+2"
-        case "EST" => "GMT+1"  // FIXME ??
-        case a => a }))
-
-    Date.Format.make(fmts, tune)
-  }
-
   object Isatest
   {
     val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
@@ -203,20 +227,13 @@
 
   private def parse_header(log_file: Log_File): Header =
   {
-    object Strict_Date
-    {
-      def unapply(s: String): Some[Date] =
-        try { Some(Date_Format.parse(s)) }
-        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
-    }
-
     def parse(kind: Kind.Value, start: Date, hostname: String,
       Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
     {
       val start_date = Field.build_start -> start.toString
       val end_date =
         log_file.lines.last match {
-          case Test_End(Strict_Date(end_date)) =>
+          case Test_End(log_file.Strict_Date(end_date)) =>
             List(Field.build_end -> end_date.toString)
           case _ => Nil
         }
@@ -236,15 +253,15 @@
     }
 
     log_file.lines match {
-      case Isatest.Test_Start(Strict_Date(start), hostname) :: _ =>
+      case Isatest.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
         parse(Kind.ISATEST, start, hostname,
           Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
 
-      case AFP.Test_Start(Strict_Date(start), hostname) :: _ =>
+      case AFP.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
         parse(Kind.AFP_TEST, start, hostname,
           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
 
-      case AFP.Test_Start_Old(Strict_Date(start)) :: _ =>
+      case AFP.Test_Start_Old(log_file.Strict_Date(start)) :: _ =>
         parse(Kind.AFP_TEST, start, "",
           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)