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