author | wenzelm |
Tue, 21 Apr 2020 22:04:15 +0200 | |
changeset 71776 | 5ef7f374e0f8 |
parent 71775 | 291c46bf3000 |
child 71777 | 3875815f5967 |
--- a/src/Pure/General/json.scala Tue Apr 21 19:07:49 2020 +0200 +++ b/src/Pure/General/json.scala Tue Apr 21 22:04:15 2020 +0200 @@ -29,7 +29,7 @@ def apply(entries: Entry*): Object.T = Map(entries:_*) - def unapply(obj: T): Option[Object.T] = + def unapply(obj: Any): Option[Object.T] = obj match { case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => Some(m.asInstanceOf[Object.T])