changeset 71382 | 6316debd3a9f |
parent 70536 | fe4d545f12e3 |
child 73023 | e15621aa8c72 |
--- a/src/Pure/General/cache.scala Wed Jan 15 19:46:04 2020 +0100 +++ b/src/Pure/General/cache.scala Wed Jan 15 19:49:13 2020 +0100 @@ -24,11 +24,7 @@ { val ref = table.get(x) if (ref == null) None - else { - val y = ref.asInstanceOf[WeakReference[A]].get - if (y == null) None - else Some(y) - } + else Option(ref.asInstanceOf[WeakReference[A]].get) } protected def store[A](x: A): A =