# HG changeset patch
# User wenzelm
# Date 1709928935 -3600
# Node ID e7940d49fe744bca598c5aafda1f1e11a670749e
# Parent  141df3fb25bfe2cb2891b0247b0e325f22b45412
clarified signature;

diff -r 141df3fb25bf -r e7940d49fe74 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Mar 08 20:38:19 2024 +0100
+++ b/src/Pure/General/date.scala	Fri Mar 08 21:15:35 2024 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/date.scala
     Author:     Makarius
 
-Date and time, with time zone.
+Date and time, with timezone.
 */
 
 package isabelle
@@ -91,19 +91,21 @@
 
   def timezone(): ZoneId = ZoneId.systemDefault
 
-  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
+  def now(timezone: ZoneId = Date.timezone()): Date =
+    new Date(ZonedDateTime.now(timezone))
 
-  def instant(t: Instant, zone: ZoneId = timezone()): Date =
-    new Date(ZonedDateTime.ofInstant(t, zone))
+  def instant(t: Instant, timezone: ZoneId = Date.timezone()): Date =
+    new Date(ZonedDateTime.ofInstant(t, timezone))
 
-  def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
+  def apply(t: Time, timezone: ZoneId = Date.timezone()): Date =
+    instant(t.instant, timezone)
 }
 
 sealed case class Date(rep: ZonedDateTime) {
   def midnight: Date =
     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
 
-  def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
+  def to(other: ZoneId): Date = new Date(rep.withZoneSameInstant(other))
 
   def unix_epoch: Long = rep.toEpochSecond
   def unix_epoch_day: Long = rep.toLocalDate.toEpochDay
@@ -111,8 +113,8 @@
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
 
-  def + (t: Time): Date = Date(time + t, zone = timezone)
-  def - (t: Time): Date = Date(time - t, zone = timezone)
+  def + (t: Time): Date = Date(time + t, timezone = timezone)
+  def - (t: Time): Date = Date(time - t, timezone = timezone)
   def - (d: Date): Time = time - d.time
 
   def format(fmt: Date.Format = Date.Format.default): String = fmt(this)