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.sql.Timestamp
|
|
12 |
import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
|
64056
|
13 |
import java.time.format.{DateTimeFormatter, DateTimeParseException}
|
64059
|
14 |
import java.time.temporal.TemporalAccessor
|
|
15 |
|
|
16 |
import scala.annotation.tailrec
|
64056
|
17 |
|
|
18 |
|
|
19 |
object Date
|
|
20 |
{
|
|
21 |
/* format */
|
|
22 |
|
|
23 |
object Format
|
|
24 |
{
|
64098
|
25 |
def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
|
64059
|
26 |
{
|
|
27 |
require(fmts.nonEmpty)
|
|
28 |
|
64056
|
29 |
new Format {
|
64059
|
30 |
def apply(date: Date): String = fmts.head.format(date.rep)
|
|
31 |
def parse(str: String): Date =
|
64098
|
32 |
new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
|
64056
|
33 |
}
|
64059
|
34 |
}
|
64056
|
35 |
|
64098
|
36 |
def apply(pats: String*): Format =
|
|
37 |
make(pats.toList.map(Date.Formatter.pattern(_)))
|
64060
|
38 |
|
64098
|
39 |
val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
|
|
40 |
val date: Format = Format("dd-MMM-uuuu")
|
|
41 |
val time: Format = Format("HH:mm:ss")
|
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)
|
|
60 |
if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
|
|
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 |
|
|
79 |
def timezone(): ZoneId = ZoneId.systemDefault
|
|
80 |
|
|
81 |
def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
|
|
82 |
|
65014
|
83 |
def instant(t: Instant, zone: ZoneId = timezone()): Date =
|
|
84 |
new Date(ZonedDateTime.ofInstant(t, zone))
|
|
85 |
|
|
86 |
def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
|
64056
|
87 |
}
|
|
88 |
|
64059
|
89 |
sealed case class Date(rep: ZonedDateTime)
|
64056
|
90 |
{
|
64117
|
91 |
def midnight: Date =
|
|
92 |
new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
|
|
93 |
|
64111
|
94 |
def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
|
|
95 |
def to_utc: Date = to(ZoneId.of("UTC"))
|
|
96 |
|
65014
|
97 |
def instant: Instant = Instant.from(rep)
|
|
98 |
def timestamp: Timestamp = Timestamp.from(instant)
|
|
99 |
def time: Time = Time.instant(instant)
|
64057
|
100 |
def timezone: ZoneId = rep.getZone
|
|
101 |
|
|
102 |
def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
|
|
103 |
override def toString: String = format()
|
64056
|
104 |
}
|