# HG changeset patch
# User wenzelm
# Date 1475874680 -7200
# Node ID 5edeb60a7ec5062c91608696536bbaed39a7b72d
# Parent  1a6d37c31df9c96f94cbe787be0cf4f809fa3876
more flexible date formats;

diff -r 1a6d37c31df9 -r 5edeb60a7ec5 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Oct 07 22:58:24 2016 +0200
+++ b/src/Pure/General/date.scala	Fri Oct 07 23:11:20 2016 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.util.Locale
 import java.time.{Instant, ZonedDateTime, ZoneId}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.time.temporal.TemporalAccessor
@@ -41,8 +42,18 @@
       }
     }
 
-    def make_patterns(patterns: List[String], filter: String => String = s => s): Format =
-      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)), filter)
+    def make_variants(patterns: List[String],
+      locales: List[Locale] = List(Locale.ROOT),
+      filter: String => String = s => s): Format =
+    {
+      val fmts =
+        patterns.flatMap(pat =>
+          {
+            val fmt = DateTimeFormatter.ofPattern(pat)
+            locales.map(fmt.withLocale(_))
+          })
+      make(fmts, filter)
+    }
 
     def apply(patterns: String*): Format =
       make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
diff -r 1a6d37c31df9 -r 5edeb60a7ec5 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 22:58:24 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 23:11:20 2016 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.util.Locale
 import java.io.{File => JFile}
 import java.time.ZonedDateTime
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
@@ -182,7 +183,9 @@
   /* header and meta data */
 
   val Date_Format =
-    Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
+    Date.Format.make_variants(
+      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
+      List(Locale.ENGLISH, Locale.GERMAN),
       // workaround for jdk-8u102
       s => Word.implode(Word.explode(s).map({
         case "CET" | "MET" => "GMT+1"