# HG changeset patch
# User wenzelm
# Date 1475694128 -7200
# Node ID 365d367d2b45c79226bc7dd39a483bb1dc838323
# Parent  ea528dc9962d736a00ed868d7b7ed66107830653
more flexibile formatting;
expose representation for free-form formatters;

diff -r ea528dc9962d -r 365d367d2b45 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Wed Oct 05 20:13:32 2016 +0200
+++ b/src/Pure/General/date.scala	Wed Oct 05 21:02:08 2016 +0200
@@ -9,6 +9,9 @@
 
 import java.time.{Instant, ZonedDateTime, ZoneId}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
+import java.time.temporal.TemporalAccessor
+
+import scala.annotation.tailrec
 
 
 object Date
@@ -17,14 +20,29 @@
 
   object Format
   {
-    def apply(fmt: DateTimeFormatter): Format =
+    def make(fmts: List[DateTimeFormatter]): Format =
+    {
+      require(fmts.nonEmpty)
+
+      @tailrec def parse_first(
+        last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor =
+      {
+        fs match {
+          case Nil => throw last_exn.get
+          case f :: rest =>
+            try { ZonedDateTime.from(f.parse(str)) }
+            catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) }
+        }
+      }
       new Format {
-        def apply(date: Date): String = fmt.format(date.rep)
-        def parse(str: String): Date = new Date(ZonedDateTime.from(fmt.parse(str)))
+        def apply(date: Date): String = fmts.head.format(date.rep)
+        def parse(str: String): Date =
+          new Date(ZonedDateTime.from(parse_first(None, fmts, str)))
       }
+    }
 
-    def apply(pattern: String): Format =
-      apply(DateTimeFormatter.ofPattern(pattern))
+    def apply(patterns: String*): Format =
+      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
 
     val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
     val date: Format = apply("dd-MMM-uuuu")
@@ -51,7 +69,7 @@
     new Date(ZonedDateTime.ofInstant(t.instant, zone))
 }
 
-sealed case class Date private(private[Date] rep: ZonedDateTime)
+sealed case class Date(rep: ZonedDateTime)
 {
   def time: Time = Time.instant(Instant.from(rep))
   def timezone: ZoneId = rep.getZone