src/Pure/General/date.scala
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (2 months ago)
changeset 69980 f2e3adfd916f
parent 65733 45b8446a8b52
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/General/date.scala
     2     Author:     Makarius
     3 
     4 Date and time, with time zone.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.Locale
    11 import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
    12 import java.time.format.{DateTimeFormatter, DateTimeParseException}
    13 import java.time.temporal.TemporalAccessor
    14 
    15 import scala.annotation.tailrec
    16 
    17 
    18 object 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 
    91 sealed 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 }