more date and time operations from Java 8;
authorwenzelm
Wed Oct 05 19:45:36 2016 +0200 (2016-10-05)
changeset 640560edc966bee55
parent 64055 acd3e25975a2
child 64057 fd73e0019605
more date and time operations from Java 8;
src/Pure/Concurrent/event_timer.scala
src/Pure/General/date.scala
src/Pure/General/time.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 14:34:42 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 19:45:36 2016 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.util.{Timer, TimerTask, Date}
     1.8 +import java.util.{Timer, TimerTask, Date => JDate}
     1.9  
    1.10  
    1.11  object Event_Timer
    1.12 @@ -26,7 +26,7 @@
    1.13    def request(time: Time)(event: => Unit): Request =
    1.14    {
    1.15      val task = new TimerTask { def run { event } }
    1.16 -    event_timer.schedule(task, new Date(time.ms))
    1.17 +    event_timer.schedule(task, new JDate(time.ms))
    1.18      new Request(time, task)
    1.19    }
    1.20  }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/date.scala	Wed Oct 05 19:45:36 2016 +0200
     2.3 @@ -0,0 +1,55 @@
     2.4 +/*  Title:      Pure/General/date.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Date and time, with time zone.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.time.{ZonedDateTime, ZoneId}
    2.14 +import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.15 +
    2.16 +
    2.17 +object Date
    2.18 +{
    2.19 +  def timezone(): ZoneId = ZoneId.systemDefault
    2.20 +
    2.21 +  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
    2.22 +
    2.23 +  def apply(t: Time, zone: ZoneId = timezone()): Date =
    2.24 +    new Date(ZonedDateTime.ofInstant(t.instant, zone))
    2.25 +
    2.26 +
    2.27 +  /* format */
    2.28 +
    2.29 +  object Format
    2.30 +  {
    2.31 +    def apply(fmt: DateTimeFormatter): Format =
    2.32 +      new Format {
    2.33 +        def apply(date: Date): String = fmt.format(date.rep)
    2.34 +        def parse(str: String): Date = new Date(ZonedDateTime.from(fmt.parse(str)))
    2.35 +      }
    2.36 +
    2.37 +    def apply(pattern: String): Format =
    2.38 +      apply(DateTimeFormatter.ofPattern(pattern))
    2.39 +
    2.40 +    val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
    2.41 +    val default_date: Format = apply("dd-MMM-uuuu")
    2.42 +    val default_time: Format = apply("HH:mm:ss")
    2.43 +  }
    2.44 +
    2.45 +  abstract class Format private
    2.46 +  {
    2.47 +    def apply(date: Date): String
    2.48 +    def parse(str: String): Date
    2.49 +    def unapply(str: String): Option[Date] =
    2.50 +      try { Some(parse(str)) }
    2.51 +      catch { case _: DateTimeParseException => None }
    2.52 +  }
    2.53 +}
    2.54 +
    2.55 +sealed case class Date private(private[Date] rep: ZonedDateTime)
    2.56 +{
    2.57 +  override def toString: String = Date.Format.default(this)
    2.58 +}
     3.1 --- a/src/Pure/General/time.scala	Wed Oct 05 14:34:42 2016 +0200
     3.2 +++ b/src/Pure/General/time.scala	Wed Oct 05 19:45:36 2016 +0200
     3.3 @@ -9,6 +9,7 @@
     3.4  
     3.5  
     3.6  import java.util.Locale
     3.7 +import java.time.Instant
     3.8  
     3.9  
    3.10  object Time
    3.11 @@ -25,6 +26,8 @@
    3.12  
    3.13    def print_seconds(s: Double): String =
    3.14      String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    3.15 +
    3.16 +  def instant(t: Instant): Time = ms(t.getEpochSecond + t.getNano / 1000000L)
    3.17  }
    3.18  
    3.19  final class Time private(val ms: Long) extends AnyVal
    3.20 @@ -57,4 +60,6 @@
    3.21      String.format(Locale.ROOT, "%d:%02d:%02d",
    3.22        new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
    3.23    }
    3.24 +
    3.25 +  def instant: Instant = Instant.ofEpochMilli(ms)
    3.26  }
     4.1 --- a/src/Pure/build-jars	Wed Oct 05 14:34:42 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Wed Oct 05 19:45:36 2016 +0200
     4.3 @@ -27,6 +27,7 @@
     4.4    General/antiquote.scala
     4.5    General/bytes.scala
     4.6    General/completion.scala
     4.7 +  General/date.scala
     4.8    General/exn.scala
     4.9    General/file.scala
    4.10    General/graph.scala