# HG changeset patch
# User wenzelm
# Date 1512139741 -3600
# Node ID 5fce3a24e476f866c30a5557d8b15254d1d15c78
# Parent  6b350c594ae3973a56efc773cf68f8b0d95079ed
proper synchronized Map: this may be used on multiple threads;

diff -r 6b350c594ae3 -r 5fce3a24e476 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Nov 30 17:00:19 2017 +0100
+++ b/src/Pure/PIDE/xml.scala	Fri Dec 01 15:49:01 2017 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.util.WeakHashMap
+import java.util.{Collections, WeakHashMap}
 import java.lang.ref.WeakReference
 import javax.xml.parsers.DocumentBuilderFactory
 
@@ -146,7 +146,8 @@
 
   class Cache(initial_size: Int = 131071, max_string: Int = 100)
   {
-    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
+    private val table =
+      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
 
     private def lookup[A](x: A): Option[A] =
     {