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