more flexible date formats;
authorwenzelm
Fri Oct 07 23:11:20 2016 +0200 (2016-10-07)
changeset 640965edeb60a7ec5
parent 64095 1a6d37c31df9
child 64097 331fbf2a0d2d
child 64098 099518e8af2c
more flexible date formats;
src/Pure/General/date.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Fri Oct 07 22:58:24 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Fri Oct 07 23:11:20 2016 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.util.Locale
     1.8  import java.time.{Instant, ZonedDateTime, ZoneId}
     1.9  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.10  import java.time.temporal.TemporalAccessor
    1.11 @@ -41,8 +42,18 @@
    1.12        }
    1.13      }
    1.14  
    1.15 -    def make_patterns(patterns: List[String], filter: String => String = s => s): Format =
    1.16 -      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)), filter)
    1.17 +    def make_variants(patterns: List[String],
    1.18 +      locales: List[Locale] = List(Locale.ROOT),
    1.19 +      filter: String => String = s => s): Format =
    1.20 +    {
    1.21 +      val fmts =
    1.22 +        patterns.flatMap(pat =>
    1.23 +          {
    1.24 +            val fmt = DateTimeFormatter.ofPattern(pat)
    1.25 +            locales.map(fmt.withLocale(_))
    1.26 +          })
    1.27 +      make(fmts, filter)
    1.28 +    }
    1.29  
    1.30      def apply(patterns: String*): Format =
    1.31        make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 22:58:24 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 23:11:20 2016 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.util.Locale
     2.8  import java.io.{File => JFile}
     2.9  import java.time.ZonedDateTime
    2.10  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.11 @@ -182,7 +183,9 @@
    2.12    /* header and meta data */
    2.13  
    2.14    val Date_Format =
    2.15 -    Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.16 +    Date.Format.make_variants(
    2.17 +      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.18 +      List(Locale.ENGLISH, Locale.GERMAN),
    2.19        // workaround for jdk-8u102
    2.20        s => Word.implode(Word.explode(s).map({
    2.21          case "CET" | "MET" => "GMT+1"