accept spurious empty logs;
authorwenzelm
Sat Oct 08 13:05:05 2016 +0200 (2016-10-08)
changeset 6410360d163f38056
parent 64102 1ec2adddf16b
child 64104 b70fa05d6746
accept spurious empty logs;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 12:34:07 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 13:05:05 2016 +0200
     1.3 @@ -207,6 +207,9 @@
     1.4    }
     1.5  
     1.6    sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
     1.7 +  {
     1.8 +    def is_empty: Boolean = props.isEmpty && settings.isEmpty
     1.9 +  }
    1.10  
    1.11    object Isatest
    1.12    {
    1.13 @@ -257,6 +260,8 @@
    1.14          parse(Kind.ISATEST, start, hostname,
    1.15            Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    1.16  
    1.17 +      case List(Isatest.Test_End(_)) => Header(Kind.ISATEST, Nil, Nil)
    1.18 +
    1.19        case AFP.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
    1.20          parse(Kind.AFP_TEST, start, hostname,
    1.21            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)