# HG changeset patch # User wenzelm # Date 1475924705 -7200 # Node ID 60d163f380563a8797f9ec372217d5f1217c00a6 # Parent 1ec2adddf16b39b1631c25313b969ba713041344 accept spurious empty logs; diff -r 1ec2adddf16b -r 60d163f38056 src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Sat Oct 08 12:34:07 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Sat Oct 08 13:05:05 2016 +0200 @@ -207,6 +207,9 @@ } sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)]) + { + def is_empty: Boolean = props.isEmpty && settings.isEmpty + } object Isatest { @@ -257,6 +260,8 @@ parse(Kind.ISATEST, start, hostname, Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version) + case List(Isatest.Test_End(_)) => Header(Kind.ISATEST, Nil, Nil) + 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)