src/Pure/Tools/build_log.scala
changeset 64095 1a6d37c31df9
parent 64094 629558a1ecf5
child 64096 5edeb60a7ec5
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 21:46:42 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 22:58:24 2016 +0200
     1.3 @@ -181,6 +181,15 @@
     1.4  
     1.5    /* header and meta data */
     1.6  
     1.7 +  val Date_Format =
     1.8 +    Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
     1.9 +      // workaround for jdk-8u102
    1.10 +      s => Word.implode(Word.explode(s).map({
    1.11 +        case "CET" | "MET" => "GMT+1"
    1.12 +        case "CEST" | "MEST" => "GMT+2"
    1.13 +        case "EST" => "GMT+1"  // FIXME ??
    1.14 +        case a => a })))
    1.15 +
    1.16    object Header_Kind extends Enumeration
    1.17    {
    1.18      val ISATEST = Value("isatest")
    1.19 @@ -200,17 +209,16 @@
    1.20      val afp_version = "afp_version"
    1.21    }
    1.22  
    1.23 +  object Isatest
    1.24 +  {
    1.25 +    val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
    1.26 +    val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
    1.27 +    val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
    1.28 +    val No_AFP_Version = new Regex("""$.""")
    1.29 +  }
    1.30 +
    1.31    object AFP
    1.32    {
    1.33 -    val Date_Format =
    1.34 -      Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.35 -        // workaround for jdk-8u102
    1.36 -        s => Word.implode(Word.explode(s).map({
    1.37 -          case "CET" | "MET" => "GMT+1"
    1.38 -          case "CEST" | "MEST" => "GMT+2"
    1.39 -          case "EST" => "GMT+1"  // FIXME ??
    1.40 -          case a => a })))
    1.41 -
    1.42      val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
    1.43      val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
    1.44      val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
    1.45 @@ -220,12 +228,13 @@
    1.46  
    1.47    private def parse_header(log_file: Log_File): Header =
    1.48    {
    1.49 -    def parse_afp(start: Date, hostname: String): Header =
    1.50 +    def parse(kind: Header_Kind.Value, start: Date, hostname: String,
    1.51 +      Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
    1.52      {
    1.53        val start_date = Field.build_start -> start.toString
    1.54        val end_date =
    1.55          log_file.lines.last match {
    1.56 -          case AFP.Test_End(AFP.Date_Format.Strict(end_date)) =>
    1.57 +          case Test_End(Date_Format.Strict(end_date)) =>
    1.58              List(Field.build_end -> end_date.toString)
    1.59            case _ => Nil
    1.60          }
    1.61 @@ -233,21 +242,27 @@
    1.62        val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
    1.63  
    1.64        val isabelle_version =
    1.65 -        log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _)
    1.66 +        log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
    1.67  
    1.68        val afp_version =
    1.69 -        log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _)
    1.70 +        log_file.find_match(AFP_Version).map(Field.afp_version -> _)
    1.71  
    1.72 -      Header(Header_Kind.AFP_TEST,
    1.73 -        start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList,
    1.74 +      Header(kind,
    1.75 +        start_date :: end_date ::: build_host :::
    1.76 +          isabelle_version.toList ::: afp_version.toList,
    1.77          log_file.get_settings(Settings.all_settings))
    1.78      }
    1.79  
    1.80      log_file.lines match {
    1.81 -      case AFP.Test_Start(AFP.Date_Format.Strict(start_date), hostname) :: _ =>
    1.82 -        parse_afp(start_date, hostname)
    1.83 -      case AFP.Test_Start_Old(AFP.Date_Format.Strict(start_date)) :: _ =>
    1.84 -        parse_afp(start_date, "")
    1.85 +      case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
    1.86 +        parse(Header_Kind.ISATEST, start, hostname,
    1.87 +          Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    1.88 +      case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
    1.89 +        parse(Header_Kind.AFP_TEST, start, hostname,
    1.90 +          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.91 +      case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
    1.92 +        parse(Header_Kind.AFP_TEST, start, "",
    1.93 +          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.94        case _ => log_file.err("cannot detect log header format")
    1.95      }
    1.96    }