clarified meta info;
authorwenzelm
Sat Oct 08 16:02:06 2016 +0200 (2016-10-08)
changeset 64108623abb8fecdf
parent 64107 87d32aa83410
child 64109 d54aa68e33dc
clarified meta info;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 15:46:06 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 16:02:06 2016 +0200
     1.3 @@ -211,6 +211,7 @@
     1.4  
     1.5    object Field
     1.6    {
     1.7 +    val build_engine = "build_engine"
     1.8      val build_host = "build_host"
     1.9      val build_start = "build_start"
    1.10      val build_end = "build_end"
    1.11 @@ -218,27 +219,19 @@
    1.12      val afp_version = "afp_version"
    1.13    }
    1.14  
    1.15 -  object Kind extends Enumeration
    1.16 +  object Meta_Info
    1.17    {
    1.18 -    val EMPTY = Value("empty")
    1.19 -    val ISATEST = Value("isatest")
    1.20 -    val AFP_TEST = Value("afp-test")
    1.21 -    val JENKINS = Value("jenkins")
    1.22 +    val empty: Meta_Info = Meta_Info(Nil, Nil)
    1.23    }
    1.24  
    1.25 -  object Meta_Info
    1.26 -  {
    1.27 -    val empty: Meta_Info = Meta_Info(Kind.EMPTY, Nil, Nil)
    1.28 -  }
    1.29 -
    1.30 -  sealed case class Meta_Info(
    1.31 -    kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.32 +  sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
    1.33    {
    1.34      def is_empty: Boolean = props.isEmpty && settings.isEmpty
    1.35    }
    1.36  
    1.37    object Isatest
    1.38    {
    1.39 +    val engine = "isatest"
    1.40      val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
    1.41      val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
    1.42      val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
    1.43 @@ -247,6 +240,7 @@
    1.44  
    1.45    object AFP
    1.46    {
    1.47 +    val engine = "afp-test"
    1.48      val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
    1.49      val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
    1.50      val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
    1.51 @@ -257,10 +251,13 @@
    1.52  
    1.53    private def parse_meta_info(log_file: Log_File): Meta_Info =
    1.54    {
    1.55 -    def parse(kind: Kind.Value, start: Date, hostname: String,
    1.56 +    def parse(engine: String, host: String, start: Date,
    1.57        Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
    1.58      {
    1.59 -      val start_date = Field.build_start -> start.toString
    1.60 +      val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
    1.61 +      val build_host = if (host == "") Nil else List(Field.build_host -> host)
    1.62 +
    1.63 +      val start_date = List(Field.build_start -> start.toString)
    1.64        val end_date =
    1.65          log_file.lines.last match {
    1.66            case Test_End(log_file.Strict_Date(end_date)) =>
    1.67 @@ -268,32 +265,26 @@
    1.68            case _ => Nil
    1.69          }
    1.70  
    1.71 -      val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
    1.72 -
    1.73        val isabelle_version =
    1.74          log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
    1.75 -
    1.76        val afp_version =
    1.77          log_file.find_match(AFP_Version).map(Field.afp_version -> _)
    1.78  
    1.79 -      Meta_Info(kind,
    1.80 -        start_date :: end_date ::: build_host :::
    1.81 -          isabelle_version.toList ::: afp_version.toList,
    1.82 +      Meta_Info(build_engine ::: build_host :::
    1.83 +          start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
    1.84          log_file.get_settings(Settings.all_settings))
    1.85      }
    1.86  
    1.87      log_file.lines match {
    1.88 -      case Isatest.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
    1.89 -        parse(Kind.ISATEST, start, hostname,
    1.90 -          Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    1.91 +      case Isatest.Test_Start(log_file.Strict_Date(start), host) :: _ =>
    1.92 +        parse(Isatest.engine, host, start, Isatest.Test_End,
    1.93 +          Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    1.94  
    1.95 -      case AFP.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
    1.96 -        parse(Kind.AFP_TEST, start, hostname,
    1.97 -          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.98 +      case AFP.Test_Start(log_file.Strict_Date(start), host) :: _ =>
    1.99 +        parse(AFP.engine, host, start, AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   1.100  
   1.101        case AFP.Test_Start_Old(log_file.Strict_Date(start)) :: _ =>
   1.102 -        parse(Kind.AFP_TEST, start, "",
   1.103 -          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   1.104 +        parse(AFP.engine, "", start, AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   1.105  
   1.106        case line :: _ if line.startsWith("\0") => Meta_Info.empty
   1.107        case List(Isatest.Test_End(_)) => Meta_Info.empty