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 |
{
|
|
26 |
require(fmts.nonEmpty)
|
|
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 =
|
|
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")
|
64056
|
41 |
}
|
|
42 |
|
|
43 |
abstract class Format private
|
|
44 |
{
|
|
45 |
def apply(date: Date): String
|
|
46 |
def parse(str: String): Date
|
64098
|
47 |
|
64056
|
48 |
def unapply(str: String): Option[Date] =
|
64098
|
49 |
try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
|
64056
|
50 |
}
|
64057
|
51 |
|
64099
|
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 |
|
64057
|
75 |
|
|
76 |
/* date operations */
|
|
77 |
|
|
78 |
def timezone(): ZoneId = ZoneId.systemDefault
|
|
79 |
|
|
80 |
def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
|
|
81 |
|
65014
|
82 |
def instant(t: Instant, zone: ZoneId = timezone()): Date =
|
|
83 |
new Date(ZonedDateTime.ofInstant(t, zone))
|
|
84 |
|
|
85 |
def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
|
64056
|
86 |
}
|
|
87 |
|
64059
|
88 |
sealed case class Date(rep: ZonedDateTime)
|
64056
|
89 |
{
|
64117
|
90 |
def midnight: Date =
|
|
91 |
new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
|
|
92 |
|
64111
|
93 |
def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
|
|
94 |
def to_utc: Date = to(ZoneId.of("UTC"))
|
|
95 |
|
65014
|
96 |
def instant: Instant = Instant.from(rep)
|
|
97 |
def time: Time = Time.instant(instant)
|
64057
|
98 |
def timezone: ZoneId = rep.getZone
|
|
99 |
|
|
100 |
def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
|
|
101 |
override def toString: String = format()
|
64056
|
102 |
}
|