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)) + } }