more formal directory content;
authorwenzelm
Sat Oct 08 12:20:20 2016 +0200 (2016-10-08)
changeset 64101976289c733e6
parent 64100 9b1573213ebe
child 64102 1ec2adddf16b
more formal directory content;
clarified date format;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 11:21:29 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 12:20:20 2016 +0200
     1.3 @@ -18,6 +18,19 @@
     1.4  
     1.5  object Build_Log
     1.6  {
     1.7 +  /** directory content **/
     1.8 +
     1.9 +  def is_log(file: JFile): Boolean =
    1.10 +    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
    1.11 +
    1.12 +  def isatest_files(dir: Path): List[JFile] =
    1.13 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
    1.14 +
    1.15 +  def afp_test_files(dir: Path): List[JFile] =
    1.16 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
    1.17 +
    1.18 +
    1.19 +
    1.20    /** settings **/
    1.21  
    1.22    object Settings
    1.23 @@ -90,6 +103,35 @@
    1.24        error("Error in log file " + quote(name) + ": " + msg)
    1.25  
    1.26  
    1.27 +    /* date format */
    1.28 +
    1.29 +    val Date_Format =
    1.30 +    {
    1.31 +      val fmts =
    1.32 +        Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")) ::
    1.33 +        Date.Formatter.variants(
    1.34 +          List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.35 +          List(Locale.ENGLISH, Locale.GERMAN))
    1.36 +
    1.37 +      // workaround undetected timezones
    1.38 +      def tune(s: String): String =
    1.39 +        Word.implode(Word.explode(s).map({
    1.40 +          case "CET" | "MET" => "GMT+1"
    1.41 +          case "CEST" | "MEST" => "GMT+2"
    1.42 +          case "EST" => "GMT+1"  // FIXME ??
    1.43 +          case a => a }))
    1.44 +
    1.45 +      Date.Format.make(fmts, tune)
    1.46 +    }
    1.47 +
    1.48 +    object Strict_Date
    1.49 +    {
    1.50 +      def unapply(s: String): Some[Date] =
    1.51 +        try { Some(Date_Format.parse(s)) }
    1.52 +        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
    1.53 +    }
    1.54 +
    1.55 +
    1.56      /* inlined content */
    1.57  
    1.58      def find[A](f: String => Option[A]): Option[A] =
    1.59 @@ -166,24 +208,6 @@
    1.60  
    1.61    sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.62  
    1.63 -  val Date_Format =
    1.64 -  {
    1.65 -    val fmts =
    1.66 -      Date.Formatter.variants(
    1.67 -        List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.68 -        List(Locale.ENGLISH, Locale.GERMAN))
    1.69 -
    1.70 -    // workaround undetected timezones
    1.71 -    def tune(s: String): String =
    1.72 -      Word.implode(Word.explode(s).map({
    1.73 -        case "CET" | "MET" => "GMT+1"
    1.74 -        case "CEST" | "MEST" => "GMT+2"
    1.75 -        case "EST" => "GMT+1"  // FIXME ??
    1.76 -        case a => a }))
    1.77 -
    1.78 -    Date.Format.make(fmts, tune)
    1.79 -  }
    1.80 -
    1.81    object Isatest
    1.82    {
    1.83      val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
    1.84 @@ -203,20 +227,13 @@
    1.85  
    1.86    private def parse_header(log_file: Log_File): Header =
    1.87    {
    1.88 -    object Strict_Date
    1.89 -    {
    1.90 -      def unapply(s: String): Some[Date] =
    1.91 -        try { Some(Date_Format.parse(s)) }
    1.92 -        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
    1.93 -    }
    1.94 -
    1.95      def parse(kind: Kind.Value, start: Date, hostname: String,
    1.96        Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
    1.97      {
    1.98        val start_date = Field.build_start -> start.toString
    1.99        val end_date =
   1.100          log_file.lines.last match {
   1.101 -          case Test_End(Strict_Date(end_date)) =>
   1.102 +          case Test_End(log_file.Strict_Date(end_date)) =>
   1.103              List(Field.build_end -> end_date.toString)
   1.104            case _ => Nil
   1.105          }
   1.106 @@ -236,15 +253,15 @@
   1.107      }
   1.108  
   1.109      log_file.lines match {
   1.110 -      case Isatest.Test_Start(Strict_Date(start), hostname) :: _ =>
   1.111 +      case Isatest.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
   1.112          parse(Kind.ISATEST, start, hostname,
   1.113            Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   1.114  
   1.115 -      case AFP.Test_Start(Strict_Date(start), hostname) :: _ =>
   1.116 +      case AFP.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
   1.117          parse(Kind.AFP_TEST, start, hostname,
   1.118            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   1.119  
   1.120 -      case AFP.Test_Start_Old(Strict_Date(start)) :: _ =>
   1.121 +      case AFP.Test_Start_Old(log_file.Strict_Date(start)) :: _ =>
   1.122          parse(Kind.AFP_TEST, start, "",
   1.123            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   1.124