src/Pure/General/json.scala
changeset 68943 e564605d4cac
parent 68742 a6cc4302c380
child 69458 5655af3ea5bd
     1.1 --- a/src/Pure/General/json.scala	Sat Sep 08 12:01:22 2018 +0200
     1.2 +++ b/src/Pure/General/json.scala	Sat Sep 08 12:01:37 2018 +0200
     1.3 @@ -309,6 +309,11 @@
     1.4            case _ => None
     1.5          }
     1.6      }
     1.7 +
     1.8 +    object Seconds {
     1.9 +      def unapply(json: T): Option[Time] =
    1.10 +        Double.unapply(json).map(Time.seconds(_))
    1.11 +    }
    1.12    }
    1.13  
    1.14  
    1.15 @@ -381,4 +386,9 @@
    1.16      list(obj, name, JSON.Value.String.unapply _)
    1.17    def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
    1.18      list_default(obj, name, JSON.Value.String.unapply _, default)
    1.19 +
    1.20 +  def seconds(obj: T, name: String): Option[Time] =
    1.21 +    value(obj, name, Value.Seconds.unapply)
    1.22 +  def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
    1.23 +    value_default(obj, name, Value.Seconds.unapply, default)
    1.24  }