tuned signature;
authorwenzelm
Mon Mar 25 16:45:08 2019 +0100 (2 months ago)
changeset 69980f2e3adfd916f
parent 69979 4744e75393d9
child 69981 3dced198b9ec
tuned signature;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/jenkins.scala
src/Pure/General/date.scala
src/Pure/General/sql.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 16:11:28 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 16:45:08 2019 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.time.{LocalDate, ZoneId}
     1.8 +import java.time.LocalDate
     1.9  import scala.collection.immutable.SortedMap
    1.10  
    1.11  
    1.12 @@ -31,8 +31,7 @@
    1.13    def parse_date(s: String): Date =
    1.14    {
    1.15      val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
    1.16 -    val zone_id = ZoneId.of("Europe/Berlin")
    1.17 -    Date(LocalDate.from(t).atStartOfDay(zone_id))
    1.18 +    Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
    1.19    }
    1.20  
    1.21    sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
     2.1 --- a/src/Pure/Admin/build_log.scala	Mon Mar 25 16:11:28 2019 +0100
     2.2 +++ b/src/Pure/Admin/build_log.scala	Mon Mar 25 16:45:08 2019 +0100
     2.3 @@ -8,7 +8,6 @@
     2.4  
     2.5  
     2.6  import java.io.{File => JFile}
     2.7 -import java.time.ZoneId
     2.8  import java.time.format.{DateTimeFormatter, DateTimeParseException}
     2.9  import java.util.Locale
    2.10  
    2.11 @@ -157,7 +156,7 @@
    2.12            List(Locale.ENGLISH, Locale.GERMAN)) :::
    2.13          List(
    2.14            DateTimeFormatter.RFC_1123_DATE_TIME,
    2.15 -          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    2.16 +          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin))
    2.17  
    2.18        def tune_timezone(s: String): String =
    2.19          s match {
    2.20 @@ -429,7 +428,7 @@
    2.21                log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
    2.22                  case Jenkins.Host(a, b) => a + "." + b
    2.23                }).getOrElse("")
    2.24 -            parse(Jenkins.engine, host, start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
    2.25 +            parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End,
    2.26                Jenkins.Isabelle_Version, Jenkins.AFP_Version)
    2.27            case _ => Meta_Info.empty
    2.28          }
     3.1 --- a/src/Pure/Admin/jenkins.scala	Mon Mar 25 16:11:28 2019 +0100
     3.2 +++ b/src/Pure/Admin/jenkins.scala	Mon Mar 25 16:45:08 2019 +0100
     3.3 @@ -8,7 +8,6 @@
     3.4  
     3.5  
     3.6  import java.net.URL
     3.7 -import java.time.ZoneId
     3.8  
     3.9  import scala.util.matching.Regex
    3.10  
    3.11 @@ -71,7 +70,7 @@
    3.12      main_log: URL,
    3.13      session_logs: List[(String, String, URL)])
    3.14    {
    3.15 -    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
    3.16 +    val date: Date = Date(Time.ms(timestamp), Date.timezone_berlin)
    3.17  
    3.18      def log_filename: Path =
    3.19        Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
     4.1 --- a/src/Pure/General/date.scala	Mon Mar 25 16:11:28 2019 +0100
     4.2 +++ b/src/Pure/General/date.scala	Mon Mar 25 16:45:08 2019 +0100
     4.3 @@ -75,6 +75,9 @@
     4.4  
     4.5    /* date operations */
     4.6  
     4.7 +  def timezone_utc: ZoneId = ZoneId.of("UTC")
     4.8 +  def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin")
     4.9 +
    4.10    def timezone(): ZoneId = ZoneId.systemDefault
    4.11  
    4.12    def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
    4.13 @@ -91,7 +94,6 @@
    4.14      new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
    4.15  
    4.16    def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
    4.17 -  def to_utc: Date = to(ZoneId.of("UTC"))
    4.18  
    4.19    def unix_epoch: Long = rep.toEpochSecond
    4.20    def instant: Instant = Instant.from(rep)
     5.1 --- a/src/Pure/General/sql.scala	Mon Mar 25 16:11:28 2019 +0100
     5.2 +++ b/src/Pure/General/sql.scala	Mon Mar 25 16:45:08 2019 +0100
     5.3 @@ -497,7 +497,7 @@
     5.4      // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
     5.5      def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
     5.6        if (date == null) stmt.rep.setObject(i, null)
     5.7 -      else stmt.rep.setObject(i, OffsetDateTime.from(date.to_utc.rep))
     5.8 +      else stmt.rep.setObject(i, OffsetDateTime.from(date.to(Date.timezone_utc).rep))
     5.9  
    5.10      def date(res: SQL.Result, column: SQL.Column): Date =
    5.11      {