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 |
|
|
10 |
import java.time.{ZonedDateTime, ZoneId}
|
|
11 |
import java.time.format.{DateTimeFormatter, DateTimeParseException}
|
|
12 |
|
|
13 |
|
|
14 |
object Date
|
|
15 |
{
|
|
16 |
def timezone(): ZoneId = ZoneId.systemDefault
|
|
17 |
|
|
18 |
def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
|
|
19 |
|
|
20 |
def apply(t: Time, zone: ZoneId = timezone()): Date =
|
|
21 |
new Date(ZonedDateTime.ofInstant(t.instant, zone))
|
|
22 |
|
|
23 |
|
|
24 |
/* format */
|
|
25 |
|
|
26 |
object Format
|
|
27 |
{
|
|
28 |
def apply(fmt: DateTimeFormatter): Format =
|
|
29 |
new Format {
|
|
30 |
def apply(date: Date): String = fmt.format(date.rep)
|
|
31 |
def parse(str: String): Date = new Date(ZonedDateTime.from(fmt.parse(str)))
|
|
32 |
}
|
|
33 |
|
|
34 |
def apply(pattern: String): Format =
|
|
35 |
apply(DateTimeFormatter.ofPattern(pattern))
|
|
36 |
|
|
37 |
val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
|
|
38 |
val default_date: Format = apply("dd-MMM-uuuu")
|
|
39 |
val default_time: Format = apply("HH:mm:ss")
|
|
40 |
}
|
|
41 |
|
|
42 |
abstract class Format private
|
|
43 |
{
|
|
44 |
def apply(date: Date): String
|
|
45 |
def parse(str: String): Date
|
|
46 |
def unapply(str: String): Option[Date] =
|
|
47 |
try { Some(parse(str)) }
|
|
48 |
catch { case _: DateTimeParseException => None }
|
|
49 |
}
|
|
50 |
}
|
|
51 |
|
|
52 |
sealed case class Date private(private[Date] rep: ZonedDateTime)
|
|
53 |
{
|
|
54 |
override def toString: String = Date.Format.default(this)
|
|
55 |
}
|