src/Pure/General/date.scala
changeset 64117 c2b41b073d8a
parent 64111 b2290b9d0175
child 65014 97a622d01609
--- a/src/Pure/General/date.scala	Sat Oct 08 22:08:31 2016 +0200
+++ b/src/Pure/General/date.scala	Sat Oct 08 22:36:22 2016 +0200
@@ -8,7 +8,7 @@
 
 
 import java.util.Locale
-import java.time.{Instant, ZonedDateTime, ZoneId}
+import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.time.temporal.TemporalAccessor
 
@@ -85,6 +85,9 @@
 
 sealed case class Date(rep: ZonedDateTime)
 {
+  def midnight: Date =
+    new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
+
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   def to_utc: Date = to(ZoneId.of("UTC"))