tuned;
authorwenzelm
Wed Jan 15 19:49:13 2020 +0100 (6 days ago)
changeset 713826316debd3a9f
parent 71381 b9ea2467c929
child 71383 8313dca6dee9
tuned;
src/Pure/General/cache.scala
     1.1 --- a/src/Pure/General/cache.scala	Wed Jan 15 19:46:04 2020 +0100
     1.2 +++ b/src/Pure/General/cache.scala	Wed Jan 15 19:49:13 2020 +0100
     1.3 @@ -24,11 +24,7 @@
     1.4    {
     1.5      val ref = table.get(x)
     1.6      if (ref == null) None
     1.7 -    else {
     1.8 -      val y = ref.asInstanceOf[WeakReference[A]].get
     1.9 -      if (y == null) None
    1.10 -      else Some(y)
    1.11 -    }
    1.12 +    else Option(ref.asInstanceOf[WeakReference[A]].get)
    1.13    }
    1.14  
    1.15    protected def store[A](x: A): A =