src/Pure/General/date.scala
author wenzelm
Wed Oct 05 19:45:36 2016 +0200 (2016-10-05)
changeset 64056 0edc966bee55
child 64057 fd73e0019605
permissions -rw-r--r--
more date and time operations from Java 8;
     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 }