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_utc: ZoneId = ZoneId.of("UTC") 79 def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin") 80 81 def timezone(): ZoneId = ZoneId.systemDefault 82 83 def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone)) 84 85 def instant(t: Instant, zone: ZoneId = timezone()): Date = 86 new Date(ZonedDateTime.ofInstant(t, zone)) 87 88 def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone) 89} 90 91sealed case class Date(rep: ZonedDateTime) 92{ 93 def midnight: Date = 94 new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone)) 95 96 def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) 97 98 def unix_epoch: Long = rep.toEpochSecond 99 def instant: Instant = Instant.from(rep) 100 def time: Time = Time.instant(instant) 101 def timezone: ZoneId = rep.getZone 102 103 def format(fmt: Date.Format = Date.Format.default): String = fmt(this) 104 override def toString: String = format() 105} 106