src/Pure/General/json.scala
changeset 64878 e9208a9301c0
parent 64761 ae97a5afffcc
child 66922 5a476a87a535
equal deleted inserted replaced
64877:31e9920a0dc1 64878:e9208a9301c0
   131   }
   131   }
   132 
   132 
   133 
   133 
   134   /* object values */
   134   /* object values */
   135 
   135 
       
   136   def optional(entry: (String, Option[T])): Map[String, T] =
       
   137     entry match {
       
   138       case (name, Some(x)) => Map(name -> x)
       
   139       case (_, None) => Map.empty
       
   140     }
       
   141 
   136   def value(obj: T, name: String): Option[T] =
   142   def value(obj: T, name: String): Option[T] =
   137     obj match {
   143     obj match {
   138       case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
   144       case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
   139         m.asInstanceOf[Map[String, T]].get(name)
   145         m.asInstanceOf[Map[String, T]].get(name)
   140       case _ => None
   146       case _ => None