src/Pure/General/date.scala
changeset 64094 629558a1ecf5
parent 64060 f3fa0bb3f666
child 64096 5edeb60a7ec5
--- 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))
+    }
   }