equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.util.WeakHashMap |
10 import java.util.{Collections, WeakHashMap} |
11 import java.lang.ref.WeakReference |
11 import java.lang.ref.WeakReference |
12 import javax.xml.parsers.DocumentBuilderFactory |
12 import javax.xml.parsers.DocumentBuilderFactory |
13 |
13 |
14 |
14 |
15 object XML |
15 object XML |
144 |
144 |
145 /** cache for partial sharing (weak table) **/ |
145 /** cache for partial sharing (weak table) **/ |
146 |
146 |
147 class Cache(initial_size: Int = 131071, max_string: Int = 100) |
147 class Cache(initial_size: Int = 131071, max_string: Int = 100) |
148 { |
148 { |
149 private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size) |
149 private val table = |
|
150 Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) |
150 |
151 |
151 private def lookup[A](x: A): Option[A] = |
152 private def lookup[A](x: A): Option[A] = |
152 { |
153 { |
153 val ref = table.get(x) |
154 val ref = table.get(x) |
154 if (ref == null) None |
155 if (ref == null) None |