more operations;
authorwenzelm
Fri Dec 01 20:41:59 2017 +0100 (10 months ago)
changeset 6711379ab935a7e22
parent 67112 deb2fcbda16e
child 67114 3d8626cbaff8
more operations;
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/PIDE/xml.scala	Fri Dec 01 20:29:58 2017 +0100
     1.2 +++ b/src/Pure/PIDE/xml.scala	Fri Dec 01 20:41:59 2017 +0100
     1.3 @@ -149,6 +149,8 @@
     1.4      private val table =
     1.5        Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
     1.6  
     1.7 +    def size: Int = table.size
     1.8 +
     1.9      private def lookup[A](x: A): Option[A] =
    1.10      {
    1.11        val ref = table.get(x)