author | wenzelm |
Fri, 08 Mar 2024 20:28:29 +0100 | |
changeset 79817 | 7308e402451f |
parent 79816 | 11fa48986f37 |
child 79818 | 0c2a62a9f136 |
--- a/src/Pure/General/date.scala Fri Mar 08 20:03:21 2024 +0100 +++ b/src/Pure/General/date.scala Fri Mar 08 20:28:29 2024 +0100 @@ -111,6 +111,10 @@ 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 - (d: Date): Time = time - d.time + def format(fmt: Date.Format = Date.Format.default): String = fmt(this) override def toString: String = format() }