# HG changeset patch
# User wenzelm
# Date 1553528708 -3600
# Node ID f2e3adfd916f2736c45ed50555c1195561451dc1
# Parent  4744e75393d97db0e507fe63eebbd9dc2f20feef
tuned signature;

diff -r 4744e75393d9 -r f2e3adfd916f src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 16:11:28 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 16:45:08 2019 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.time.{LocalDate, ZoneId}
+import java.time.LocalDate
 import scala.collection.immutable.SortedMap
 
 
@@ -31,8 +31,7 @@
   def parse_date(s: String): Date =
   {
     val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
-    val zone_id = ZoneId.of("Europe/Berlin")
-    Date(LocalDate.from(t).atStartOfDay(zone_id))
+    Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
   }
 
   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
diff -r 4744e75393d9 -r f2e3adfd916f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 25 16:11:28 2019 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 25 16:45:08 2019 +0100
@@ -8,7 +8,6 @@
 
 
 import java.io.{File => JFile}
-import java.time.ZoneId
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.util.Locale
 
@@ -157,7 +156,7 @@
           List(Locale.ENGLISH, Locale.GERMAN)) :::
         List(
           DateTimeFormatter.RFC_1123_DATE_TIME,
-          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
+          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin))
 
       def tune_timezone(s: String): String =
         s match {
@@ -429,7 +428,7 @@
               log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
                 case Jenkins.Host(a, b) => a + "." + b
               }).getOrElse("")
-            parse(Jenkins.engine, host, start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
+            parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End,
               Jenkins.Isabelle_Version, Jenkins.AFP_Version)
           case _ => Meta_Info.empty
         }
diff -r 4744e75393d9 -r f2e3adfd916f src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon Mar 25 16:11:28 2019 +0100
+++ b/src/Pure/Admin/jenkins.scala	Mon Mar 25 16:45:08 2019 +0100
@@ -8,7 +8,6 @@
 
 
 import java.net.URL
-import java.time.ZoneId
 
 import scala.util.matching.Regex
 
@@ -71,7 +70,7 @@
     main_log: URL,
     session_logs: List[(String, String, URL)])
   {
-    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
+    val date: Date = Date(Time.ms(timestamp), Date.timezone_berlin)
 
     def log_filename: Path =
       Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
diff -r 4744e75393d9 -r f2e3adfd916f src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Mon Mar 25 16:11:28 2019 +0100
+++ b/src/Pure/General/date.scala	Mon Mar 25 16:45:08 2019 +0100
@@ -75,6 +75,9 @@
 
   /* date operations */
 
+  def timezone_utc: ZoneId = ZoneId.of("UTC")
+  def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin")
+
   def timezone(): ZoneId = ZoneId.systemDefault
 
   def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
@@ -91,7 +94,6 @@
     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
 
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
-  def to_utc: Date = to(ZoneId.of("UTC"))
 
   def unix_epoch: Long = rep.toEpochSecond
   def instant: Instant = Instant.from(rep)
diff -r 4744e75393d9 -r f2e3adfd916f src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 25 16:11:28 2019 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 25 16:45:08 2019 +0100
@@ -497,7 +497,7 @@
     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
       if (date == null) stmt.rep.setObject(i, null)
-      else stmt.rep.setObject(i, OffsetDateTime.from(date.to_utc.rep))
+      else stmt.rep.setObject(i, OffsetDateTime.from(date.to(Date.timezone_utc).rep))
 
     def date(res: SQL.Result, column: SQL.Column): Date =
     {