src/Pure/General/time.scala
changeset 79775 752806151432
parent 78888 95bbf9a576b3
--- 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 {