equal
deleted
inserted
replaced
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.util.Locale |
10 import java.util.Locale |
11 import java.time.{Instant, ZonedDateTime, ZoneId} |
11 import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId} |
12 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
12 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
13 import java.time.temporal.TemporalAccessor |
13 import java.time.temporal.TemporalAccessor |
14 |
14 |
15 import scala.annotation.tailrec |
15 import scala.annotation.tailrec |
16 |
16 |
83 new Date(ZonedDateTime.ofInstant(t.instant, zone)) |
83 new Date(ZonedDateTime.ofInstant(t.instant, zone)) |
84 } |
84 } |
85 |
85 |
86 sealed case class Date(rep: ZonedDateTime) |
86 sealed case class Date(rep: ZonedDateTime) |
87 { |
87 { |
|
88 def midnight: Date = |
|
89 new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone)) |
|
90 |
88 def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) |
91 def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) |
89 def to_utc: Date = to(ZoneId.of("UTC")) |
92 def to_utc: Date = to(ZoneId.of("UTC")) |
90 |
93 |
91 def time: Time = Time.instant(Instant.from(rep)) |
94 def time: Time = Time.instant(Instant.from(rep)) |
92 def timezone: ZoneId = rep.getZone |
95 def timezone: ZoneId = rep.getZone |