# 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)