# HG changeset patch
# User wenzelm
# Date 1512157319 -3600
# Node ID 79ab935a7e22cc5fcf9d8c622163c0f2540fb9eb
# Parent  deb2fcbda16e00e6ac172ac3c671fbe489fb2415
more operations;

diff -r deb2fcbda16e -r 79ab935a7e22 src/Pure/PIDE/xml.scala
--- 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)