src/Pure/General/date.scala
author wenzelm
Sat, 04 Sep 2021 21:25:08 +0200
changeset 74232 1091880266e5
parent 73649 029de1598940
child 74925 4bc306cb2832
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/date.scala
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     3
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     4
Date and time, with time zone.
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     5
*/
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     6
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     7
package isabelle
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     8
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
     9
64096
5edeb60a7ec5 more flexible date formats;
wenzelm
parents: 64094
diff changeset
    10
import java.util.Locale
65014
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
    11
import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    12
import java.time.format.{DateTimeFormatter, DateTimeParseException}
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    13
import java.time.temporal.TemporalAccessor
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    14
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    15
import scala.annotation.tailrec
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    16
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    17
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    18
object Date
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    19
{
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    20
  /* format */
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    21
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    22
  object Format
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    23
  {
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    24
    def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    25
    {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 71601
diff changeset
    26
      require(fmts.nonEmpty, "no date formats")
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    27
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    28
      new Format {
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    29
        def apply(date: Date): String = fmts.head.format(date.rep)
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    30
        def parse(str: String): Date =
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    31
          new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    32
      }
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    33
    }
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    34
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    35
    def apply(pats: String*): Format =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
    36
      make(pats.toList.map(Date.Formatter.pattern))
64060
f3fa0bb3f666 tuned signature;
wenzelm
parents: 64059
diff changeset
    37
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    38
    val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    39
    val date: Format = Format("dd-MMM-uuuu")
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    40
    val time: Format = Format("HH:mm:ss")
73649
029de1598940 tuned signature;
wenzelm
parents: 73120
diff changeset
    41
    val alt_date: Format = Format("uuuuMMdd")
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    42
  }
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    43
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    44
  abstract class Format private
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    45
  {
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    46
    def apply(date: Date): String
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    47
    def parse(str: String): Date
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    48
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    49
    def unapply(str: String): Option[Date] =
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
    50
      try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    51
  }
64057
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    52
64099
wenzelm
parents: 64098
diff changeset
    53
  object Formatter
wenzelm
parents: 64098
diff changeset
    54
  {
wenzelm
parents: 64098
diff changeset
    55
    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
wenzelm
parents: 64098
diff changeset
    56
wenzelm
parents: 64098
diff changeset
    57
    def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
wenzelm
parents: 64098
diff changeset
    58
      pats.flatMap(pat => {
wenzelm
parents: 64098
diff changeset
    59
        val fmt = pattern(pat)
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69980
diff changeset
    60
        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
64099
wenzelm
parents: 64098
diff changeset
    61
      })
wenzelm
parents: 64098
diff changeset
    62
wenzelm
parents: 64098
diff changeset
    63
    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
wenzelm
parents: 64098
diff changeset
    64
      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
wenzelm
parents: 64098
diff changeset
    65
    {
wenzelm
parents: 64098
diff changeset
    66
      fmts match {
wenzelm
parents: 64098
diff changeset
    67
        case Nil =>
wenzelm
parents: 64098
diff changeset
    68
          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
wenzelm
parents: 64098
diff changeset
    69
        case fmt :: rest =>
wenzelm
parents: 64098
diff changeset
    70
          try { ZonedDateTime.from(fmt.parse(str)) }
wenzelm
parents: 64098
diff changeset
    71
          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
wenzelm
parents: 64098
diff changeset
    72
      }
wenzelm
parents: 64098
diff changeset
    73
    }
wenzelm
parents: 64098
diff changeset
    74
  }
wenzelm
parents: 64098
diff changeset
    75
64057
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    76
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    77
  /* date operations */
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    78
69980
f2e3adfd916f tuned signature;
wenzelm
parents: 65733
diff changeset
    79
  def timezone_utc: ZoneId = ZoneId.of("UTC")
f2e3adfd916f tuned signature;
wenzelm
parents: 65733
diff changeset
    80
  def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin")
f2e3adfd916f tuned signature;
wenzelm
parents: 65733
diff changeset
    81
64057
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    82
  def timezone(): ZoneId = ZoneId.systemDefault
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    83
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    84
  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
    85
65014
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
    86
  def instant(t: Instant, zone: ZoneId = timezone()): Date =
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
    87
    new Date(ZonedDateTime.ofInstant(t, zone))
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
    88
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
    89
  def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    90
}
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    91
64059
365d367d2b45 more flexibile formatting;
wenzelm
parents: 64057
diff changeset
    92
sealed case class Date(rep: ZonedDateTime)
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
    93
{
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64111
diff changeset
    94
  def midnight: Date =
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64111
diff changeset
    95
    new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64111
diff changeset
    96
64111
b2290b9d0175 prefer local timezone;
wenzelm
parents: 64100
diff changeset
    97
  def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
b2290b9d0175 prefer local timezone;
wenzelm
parents: 64100
diff changeset
    98
65733
wenzelm
parents: 65021
diff changeset
    99
  def unix_epoch: Long = rep.toEpochSecond
65014
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
   100
  def instant: Instant = Instant.from(rep)
97a622d01609 support for type Date;
wenzelm
parents: 64117
diff changeset
   101
  def time: Time = Time.instant(instant)
64057
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
   102
  def timezone: ZoneId = rep.getZone
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
   103
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
   104
  def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
fd73e0019605 more operations;
wenzelm
parents: 64056
diff changeset
   105
  override def toString: String = format()
64056
0edc966bee55 more date and time operations from Java 8;
wenzelm
parents:
diff changeset
   106
}