src/Pure/General/date.scala
changeset 75393 87ebf5a50283
parent 74943 afd8cb7b2be1
child 75394 42267c650205
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    13 import java.time.temporal.TemporalAccessor
    13 import java.time.temporal.TemporalAccessor
    14 
    14 
    15 import scala.annotation.tailrec
    15 import scala.annotation.tailrec
    16 
    16 
    17 
    17 
    18 object Date
    18 object Date {
    19 {
       
    20   /* format */
    19   /* format */
    21 
    20 
    22   object Format
    21   object Format {
    23   {
    22     def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = {
    24     def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
       
    25     {
       
    26       require(fmts.nonEmpty, "no date formats")
    23       require(fmts.nonEmpty, "no date formats")
    27 
    24 
    28       new Format {
    25       new Format {
    29         def apply(date: Date): String = fmts.head.format(date.rep)
    26         def apply(date: Date): String = fmts.head.format(date.rep)
    30         def parse(str: String): Date =
    27         def parse(str: String): Date =
    39     val date: Format = Format("dd-MMM-uuuu")
    36     val date: Format = Format("dd-MMM-uuuu")
    40     val time: Format = Format("HH:mm:ss")
    37     val time: Format = Format("HH:mm:ss")
    41     val alt_date: Format = Format("uuuuMMdd")
    38     val alt_date: Format = Format("uuuuMMdd")
    42   }
    39   }
    43 
    40 
    44   abstract class Format private
    41   abstract class Format private {
    45   {
       
    46     def apply(date: Date): String
    42     def apply(date: Date): String
    47     def parse(str: String): Date
    43     def parse(str: String): Date
    48 
    44 
    49     def unapply(str: String): Option[Date] =
    45     def unapply(str: String): Option[Date] =
    50       try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
    46       try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
    51   }
    47   }
    52 
    48 
    53   object Formatter
    49   object Formatter {
    54   {
       
    55     def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
    50     def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
    56 
    51 
    57     def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
    52     def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
    58       pats.flatMap(pat => {
    53       pats.flatMap(pat => {
    59         val fmt = pattern(pat)
    54         val fmt = pattern(pat)
    60         if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
    55         if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
    61       })
    56       })
    62 
    57 
    63     @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
    58     @tailrec def try_variants(
    64       last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
    59       fmts: List[DateTimeFormatter],
    65     {
    60       str: String,
       
    61       last_exn: Option[DateTimeParseException] = None
       
    62     ): TemporalAccessor = {
    66       fmts match {
    63       fmts match {
    67         case Nil =>
    64         case Nil =>
    68           throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
    65           throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
    69         case fmt :: rest =>
    66         case fmt :: rest =>
    70           try { ZonedDateTime.from(fmt.parse(str)) }
    67           try { ZonedDateTime.from(fmt.parse(str)) }
    74   }
    71   }
    75 
    72 
    76 
    73 
    77   /* ordering */
    74   /* ordering */
    78 
    75 
    79   object Ordering extends scala.math.Ordering[Date]
    76   object Ordering extends scala.math.Ordering[Date] {
    80   {
       
    81     def compare(date1: Date, date2: Date): Int =
    77     def compare(date1: Date, date2: Date): Int =
    82       date1.instant.compareTo(date2.instant)
    78       date1.instant.compareTo(date2.instant)
    83   }
    79   }
    84 
    80 
    85   object Rev_Ordering extends scala.math.Ordering[Date]
    81   object Rev_Ordering extends scala.math.Ordering[Date] {
    86   {
       
    87     def compare(date1: Date, date2: Date): Int =
    82     def compare(date1: Date, date2: Date): Int =
    88       date2.instant.compareTo(date1.instant)
    83       date2.instant.compareTo(date1.instant)
    89   }
    84   }
    90 
    85 
    91 
    86 
   102     new Date(ZonedDateTime.ofInstant(t, zone))
    97     new Date(ZonedDateTime.ofInstant(t, zone))
   103 
    98 
   104   def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
    99   def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
   105 }
   100 }
   106 
   101 
   107 sealed case class Date(rep: ZonedDateTime)
   102 sealed case class Date(rep: ZonedDateTime) {
   108 {
       
   109   def midnight: Date =
   103   def midnight: Date =
   110     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
   104     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
   111 
   105 
   112   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   106   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   113 
   107