src/Pure/General/cache.scala

 
 import java.util.{Collections, WeakHashMap, Map => JMap}
 import java.lang.ref.WeakReference
 
 
-object Cache
-{
+object Cache {
   val default_max_string = 100
   val default_initial_size = 131071
 
   def make(
       max_string: Int = default_max_string,

     new Cache(max_string, initial_size)
 
   val none: Cache = make(max_string = 0)
 }
 
-class Cache(max_string: Int, initial_size: Int)
-{
+class Cache(max_string: Int, initial_size: Int) {
   val no_cache: Boolean = max_string == 0
 
   private val table: JMap[Any, WeakReference[Any]] =
     if (max_string == 0) null
     else  Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
 
   override def toString: String =
     if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")"
 
-  protected def lookup[A](x: A): Option[A] =
-  {
+  protected def lookup[A](x: A): Option[A] = {
     if (table == null) None
     else {
       val ref = table.get(x)
       if (ref == null) None
       else Option(ref.asInstanceOf[WeakReference[A]].get)
     }
   }
 
-  protected def store[A](x: A): A =
-  {
+  protected def store[A](x: A): A = {
     if (table == null || x == null) x
     else {
       table.put(x, new WeakReference[Any](x))
       x
     }
   }
 
-  protected def cache_string(x: String): String =
-  {
+  protected def cache_string(x: String): String = {
     if (x == null) null
     else if (x == "") ""
     else if (x == "true") "true"
     else if (x == "false") "false"
     else if (x == "0.0") "0.0"