# HG changeset patch
# User wenzelm
# Date 1475869602 -7200
# Node ID 629558a1ecf5c279d1b06e7d222ffaa0b5d869ec
# Parent  f09f377da49d2bc122280e14284eb3f66e4e8029
tuned;

diff -r f09f377da49d -r 629558a1ecf5 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Oct 07 21:19:15 2016 +0200
+++ b/src/Pure/General/date.scala	Fri Oct 07 21:46:42 2016 +0200
@@ -59,6 +59,10 @@
     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))
+    }
   }
 
 
diff -r f09f377da49d -r 629558a1ecf5 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 21:19:15 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 21:46:42 2016 +0200
@@ -211,11 +211,6 @@
           case "EST" => "GMT+1"  // FIXME ??
           case a => a })))
 
-    object Strict_Date
-    {
-      def unapply(s: String): Some[Date] = Some(Date_Format.parse(s))
-    }
-
     val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
     val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
     val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
@@ -230,7 +225,7 @@
       val start_date = Field.build_start -> start.toString
       val end_date =
         log_file.lines.last match {
-          case AFP.Test_End(AFP.Strict_Date(end_date)) =>
+          case AFP.Test_End(AFP.Date_Format.Strict(end_date)) =>
             List(Field.build_end -> end_date.toString)
           case _ => Nil
         }
@@ -249,9 +244,9 @@
     }
 
     log_file.lines match {
-      case AFP.Test_Start(AFP.Strict_Date(start_date), hostname) :: _ =>
+      case AFP.Test_Start(AFP.Date_Format.Strict(start_date), hostname) :: _ =>
         parse_afp(start_date, hostname)
-      case AFP.Test_Start_Old(AFP.Strict_Date(start_date)) :: _ =>
+      case AFP.Test_Start_Old(AFP.Date_Format.Strict(start_date)) :: _ =>
         parse_afp(start_date, "")
       case _ => log_file.err("cannot detect log header format")
     }