1/* Title: Pure/General/date.scala 2 Author: Makarius 3 4Date and time, with time zone. 5*/ 6 7package isabelle 8 9 10import java.util.Locale 11import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime} 12import java.time.format.{DateTimeFormatter, DateTimeParseException} 13import java.time.temporal.TemporalAccessor 14 15import scala.annotation.tailrec 16 17 18object Date 19{ 20 /* format */ 21 22 object Format 23 { 24 def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = 25 { 26 require(fmts.nonEmpty) 27 28 new Format { 29 def apply(date: Date): String = fmts.head.format(date.rep) 30 def parse(str: String): Date = 31 new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str)))) 32 } 33 } 34 35 def apply(pats: String*): Format = 36 make(pats.toList.map(Date.Formatter.pattern(_))) 37 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") 41 } 42 43 abstract class Format private 44 { 45 def apply(date: Date): String 46 def parse(str: String): Date 47 48 def unapply(str: String): Option[Date] = 49 try { Some(parse(str)) } catch { case _: DateTimeParseException => None } 50 } 51 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 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 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) 86} 87 88sealed case class Date(rep: ZonedDateTime) 89{ 90 def midnight: Date = 91 new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone)) 92 93 def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) 94 def to_utc: Date = to(ZoneId.of("UTC")) 95 96 def unix_epoch: Long = rep.toEpochSecond 97 def instant: Instant = Instant.from(rep) 98 def time: Time = Time.instant(instant) 99 def timezone: ZoneId = rep.getZone 100 101 def format(fmt: Date.Format = Date.Format.default): String = fmt(this) 102 override def toString: String = format() 103} 104