--- a/src/Pure/General/time.scala Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Pure/General/time.scala Tue Mar 05 15:54:33 2024 +0100
@@ -27,6 +27,16 @@
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
+
+ def guard_property(prop: String): Time =
+ System.getProperty(prop, "") match {
+ case Value.Seconds(t) => t
+ case "true" => Time.min
+ case "false" | "" => Time.max
+ case s =>
+ error("Bad system property " + prop + ": " + quote(s) +
+ "\n expected true, false, or time in seconds")
+ }
}
final class Time private(val ms: Long) extends AnyVal {