src/Pure/General/cache.scala

--- a/src/Pure/General/cache.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/General/cache.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -11,8 +11,7 @@
 import java.lang.ref.WeakReference
 
 
-object Cache
-{
+object Cache {
   val default_max_string = 100
   val default_initial_size = 131071
 
@@ -24,8 +23,7 @@
   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]] =
@@ -35,8 +33,7 @@
   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)
@@ -45,8 +42,7 @@
     }
   }
 
-  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))
@@ -54,8 +50,7 @@
     }
   }
 
-  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"