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] = {