author | wenzelm |
Thu, 24 May 2018 21:21:26 +0200 | |
changeset 68266 | f13bb379c573 |
parent 68265 | f0899dad4877 |
child 68267 | 6a29709906c6 |
--- a/src/Pure/General/cache.scala Thu May 24 21:13:09 2018 +0200 +++ b/src/Pure/General/cache.scala Thu May 24 21:21:26 2018 +0200 @@ -18,6 +18,8 @@ def size: Int = table.size + override def toString: String = "Cache(" + size + ")" + protected def lookup[A](x: A): Option[A] = { val ref = table.get(x)