author | wenzelm |
Fri, 01 Dec 2017 20:41:59 +0100 | |
changeset 67113 | 79ab935a7e22 |
parent 67112 | deb2fcbda16e |
child 67114 | 3d8626cbaff8 |
--- a/src/Pure/PIDE/xml.scala Fri Dec 01 20:29:58 2017 +0100 +++ b/src/Pure/PIDE/xml.scala Fri Dec 01 20:41:59 2017 +0100 @@ -149,6 +149,8 @@ private val table = Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) + def size: Int = table.size + private def lookup[A](x: A): Option[A] = { val ref = table.get(x)