1/*  Title:      Pure/General/date.scala
2    Author:     Makarius
3
4Date and time, with time zone.
5*/
6
7package isabelle
8
9
10import java.util.Locale
11import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
12import java.time.format.{DateTimeFormatter, DateTimeParseException}
13import java.time.temporal.TemporalAccessor
14
15import scala.annotation.tailrec
16
17
18object Date
19{
20  /* format */
21
22  object Format
23  {
24    def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
25    {
26      require(fmts.nonEmpty)
27
28      new Format {
29        def apply(date: Date): String = fmts.head.format(date.rep)
30        def parse(str: String): Date =
31          new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
32      }
33    }
34
35    def apply(pats: String*): Format =
36      make(pats.toList.map(Date.Formatter.pattern(_)))
37
38    val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
39    val date: Format = Format("dd-MMM-uuuu")
40    val time: Format = Format("HH:mm:ss")
41  }
42
43  abstract class Format private
44  {
45    def apply(date: Date): String
46    def parse(str: String): Date
47
48    def unapply(str: String): Option[Date] =
49      try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
50  }
51
52  object Formatter
53  {
54    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
55
56    def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
57      pats.flatMap(pat => {
58        val fmt = pattern(pat)
59        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
60      })
61
62    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
63      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
64    {
65      fmts match {
66        case Nil =>
67          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
68        case fmt :: rest =>
69          try { ZonedDateTime.from(fmt.parse(str)) }
70          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
71      }
72    }
73  }
74
75
76  /* date operations */
77
78  def timezone_utc: ZoneId = ZoneId.of("UTC")
79  def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin")
80
81  def timezone(): ZoneId = ZoneId.systemDefault
82
83  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
84
85  def instant(t: Instant, zone: ZoneId = timezone()): Date =
86    new Date(ZonedDateTime.ofInstant(t, zone))
87
88  def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
89}
90
91sealed case class Date(rep: ZonedDateTime)
92{
93  def midnight: Date =
94    new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
95
96  def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
97
98  def unix_epoch: Long = rep.toEpochSecond
99  def instant: Instant = Instant.from(rep)
100  def time: Time = Time.instant(instant)
101  def timezone: ZoneId = rep.getZone
102
103  def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
104  override def toString: String = format()
105}
106