--- a/src/Pure/General/json.scala Sat Sep 08 12:01:22 2018 +0200
+++ b/src/Pure/General/json.scala Sat Sep 08 12:01:37 2018 +0200
@@ -309,6 +309,11 @@
case _ => None
}
}
+
+ object Seconds {
+ def unapply(json: T): Option[Time] =
+ Double.unapply(json).map(Time.seconds(_))
+ }
}
@@ -381,4 +386,9 @@
list(obj, name, JSON.Value.String.unapply _)
def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
list_default(obj, name, JSON.Value.String.unapply _, default)
+
+ def seconds(obj: T, name: String): Option[Time] =
+ value(obj, name, Value.Seconds.unapply)
+ def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
+ value_default(obj, name, Value.Seconds.unapply, default)
}