tuned error;

--- a/src/Pure/General/date.scala	Sat Oct 08 11:04:47 2016 +0200
+++ b/src/Pure/General/date.scala	Sat Oct 08 11:21:29 2016 +0200
@@ -47,10 +47,6 @@
 
     def unapply(str: String): Option[Date] =
       try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
-    object Strict
-    {
-      def unapply(s: String): Some[Date] = Some(parse(s))
-    }
   }
 
   object Formatter

--- a/src/Pure/Tools/build_log.scala	Sat Oct 08 11:04:47 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 11:21:29 2016 +0200
@@ -7,8 +7,10 @@
 package isabelle
 
 
+import java.io.{File => JFile}
+import java.time.ZoneId
+import java.time.format.DateTimeParseException
 import java.util.Locale
-import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.util.matching.Regex
@@ -47,6 +49,7 @@
   }
 
 
+
   /** log file **/
 
   object Log_File
@@ -200,13 +203,20 @@
 
   private def parse_header(log_file: Log_File): Header =
   {
+    object Strict_Date
+    {
+      def unapply(s: String): Some[Date] =
+        try { Some(Date_Format.parse(s)) }
+        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
+    }
+
     def parse(kind: Kind.Value, start: Date, hostname: String,
       Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
     {
       val start_date = Field.build_start -> start.toString
       val end_date =
         log_file.lines.last match {
-          case Test_End(Date_Format.Strict(end_date)) =>
+          case Test_End(Strict_Date(end_date)) =>
             List(Field.build_end -> end_date.toString)
           case _ => Nil
         }
@@ -226,15 +236,15 @@
     }
 
     log_file.lines match {
-      case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
+      case Isatest.Test_Start(Strict_Date(start), hostname) :: _ =>
         parse(Kind.ISATEST, start, hostname,
           Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
 
-      case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
+      case AFP.Test_Start(Strict_Date(start), hostname) :: _ =>
         parse(Kind.AFP_TEST, start, hostname,
           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
 
-      case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
+      case AFP.Test_Start_Old(Strict_Date(start)) :: _ =>
         parse(Kind.AFP_TEST, start, "",
           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)