1/*  Title:      Pure/General/cache.scala
2    Author:     Makarius
3
4cache for partial sharing (weak table).
5*/
6
7package isabelle
8
9
10import java.util.{Collections, WeakHashMap}
11import java.lang.ref.WeakReference
12
13
14class Cache(initial_size: Int = 131071, max_string: Int = 100)
15{
16  private val table =
17    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
18
19  def size: Int = table.size
20
21  override def toString: String = "Cache(" + size + ")"
22
23  protected def lookup[A](x: A): Option[A] =
24  {
25    val ref = table.get(x)
26    if (ref == null) None
27    else Option(ref.asInstanceOf[WeakReference[A]].get)
28  }
29
30  protected def store[A](x: A): A =
31  {
32    table.put(x, new WeakReference[Any](x))
33    x
34  }
35
36  protected def cache_string(x: String): String =
37  {
38    if (x == "") ""
39    else if (x == "true") "true"
40    else if (x == "false") "false"
41    else if (x == "0.0") "0.0"
42    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
43    else {
44      lookup(x) match {
45        case Some(y) => y
46        case None =>
47          val z = Library.isolate_substring(x)
48          if (z.length > max_string) z else store(z)
49      }
50    }
51  }
52
53  // main methods
54  def string(x: String): String = synchronized { cache_string(x) }
55}
56