changeset 71776 | 5ef7f374e0f8 |
parent 71601 | 97ccf48c2f0c |
child 73340 | 0ffcad1f6130 |
--- 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])