proper synchronized Map: this may be used on multiple threads;
authorwenzelm
Fri Dec 01 15:49:01 2017 +0100 (6 weeks ago)
changeset 671095fce3a24e476
parent 67108 6b350c594ae3
child 67110 3156faac30a7
proper synchronized Map: this may be used on multiple threads;
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/PIDE/xml.scala	Thu Nov 30 17:00:19 2017 +0100
     1.2 +++ b/src/Pure/PIDE/xml.scala	Fri Dec 01 15:49:01 2017 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.util.WeakHashMap
     1.8 +import java.util.{Collections, WeakHashMap}
     1.9  import java.lang.ref.WeakReference
    1.10  import javax.xml.parsers.DocumentBuilderFactory
    1.11  
    1.12 @@ -146,7 +146,8 @@
    1.13  
    1.14    class Cache(initial_size: Int = 131071, max_string: Int = 100)
    1.15    {
    1.16 -    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
    1.17 +    private val table =
    1.18 +      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
    1.19  
    1.20      private def lookup[A](x: A): Option[A] =
    1.21      {