more operations;
authorwenzelm
Wed Oct 05 20:06:54 2016 +0200 (2016-10-05)
changeset 64057fd73e0019605
parent 64056 0edc966bee55
child 64058 ea528dc9962d
more operations;
tuned;
src/Pure/General/date.scala
     1.1 --- a/src/Pure/General/date.scala	Wed Oct 05 19:45:36 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Wed Oct 05 20:06:54 2016 +0200
     1.3 @@ -7,20 +7,12 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.time.{ZonedDateTime, ZoneId}
     1.8 +import java.time.{Instant, ZonedDateTime, ZoneId}
     1.9  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.10  
    1.11  
    1.12  object Date
    1.13  {
    1.14 -  def timezone(): ZoneId = ZoneId.systemDefault
    1.15 -
    1.16 -  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
    1.17 -
    1.18 -  def apply(t: Time, zone: ZoneId = timezone()): Date =
    1.19 -    new Date(ZonedDateTime.ofInstant(t.instant, zone))
    1.20 -
    1.21 -
    1.22    /* format */
    1.23  
    1.24    object Format
    1.25 @@ -35,8 +27,8 @@
    1.26        apply(DateTimeFormatter.ofPattern(pattern))
    1.27  
    1.28      val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
    1.29 -    val default_date: Format = apply("dd-MMM-uuuu")
    1.30 -    val default_time: Format = apply("HH:mm:ss")
    1.31 +    val date: Format = apply("dd-MMM-uuuu")
    1.32 +    val time: Format = apply("HH:mm:ss")
    1.33    }
    1.34  
    1.35    abstract class Format private
    1.36 @@ -47,9 +39,23 @@
    1.37        try { Some(parse(str)) }
    1.38        catch { case _: DateTimeParseException => None }
    1.39    }
    1.40 +
    1.41 +
    1.42 +  /* date operations */
    1.43 +
    1.44 +  def timezone(): ZoneId = ZoneId.systemDefault
    1.45 +
    1.46 +  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
    1.47 +
    1.48 +  def apply(t: Time, zone: ZoneId = timezone()): Date =
    1.49 +    new Date(ZonedDateTime.ofInstant(t.instant, zone))
    1.50  }
    1.51  
    1.52  sealed case class Date private(private[Date] rep: ZonedDateTime)
    1.53  {
    1.54 -  override def toString: String = Date.Format.default(this)
    1.55 +  def time: Time = Time.instant(Instant.from(rep))
    1.56 +  def timezone: ZoneId = rep.getZone
    1.57 +
    1.58 +  def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
    1.59 +  override def toString: String = format()
    1.60  }