src/Pure/General/date.scala

--- a/src/Pure/General/date.scala	Wed Oct 05 21:02:08 2016 +0200
+++ b/src/Pure/General/date.scala	Wed Oct 05 22:07:36 2016 +0200
@@ -20,7 +20,7 @@
 
   object Format
   {
-    def make(fmts: List[DateTimeFormatter]): Format =
+    def make(fmts: List[DateTimeFormatter], filter: String => String = s => s): Format =
     {
       require(fmts.nonEmpty)
 
@@ -37,10 +37,13 @@
       new Format {
         def apply(date: Date): String = fmts.head.format(date.rep)
         def parse(str: String): Date =
-          new Date(ZonedDateTime.from(parse_first(None, fmts, str)))
+          new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str))))
       }
     }
 
+    def make_patterns(patterns: List[String], filter: String => String = s => s): Format =
+      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)), filter)
+
     def apply(patterns: String*): Format =
       make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))