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