more general cache, also for term substructures;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/cache.scala	Thu May 24 21:13:09 2018 +0200
@@ -0,0 +1,61 @@
+/*  Title:      Pure/cache.scala
+    Author:     Makarius
+
+cache for partial sharing (weak table).
+*/
+
+package isabelle
+
+
+import java.util.{Collections, WeakHashMap}
+import java.lang.ref.WeakReference
+
+
+class Cache(initial_size: Int = 131071, max_string: Int = 100)
+{
+  private val table =
+    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
+
+  def size: Int = table.size
+
+  protected def lookup[A](x: A): Option[A] =
+  {
+    val ref = table.get(x)
+    if (ref == null) None
+    else {
+      val y = ref.asInstanceOf[WeakReference[A]].get
+      if (y == null) None
+      else Some(y)
+    }
+  }
+
+  protected def store[A](x: A): A =
+  {
+    table.put(x, new WeakReference[Any](x))
+    x
+  }
+
+  protected def cache_int(x: Int): Int =
+    lookup(x) getOrElse store(x)
+
+  protected def cache_string(x: String): String =
+  {
+    if (x == "") ""
+    else if (x == "true") "true"
+    else if (x == "false") "false"
+    else if (x == "0.0") "0.0"
+    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
+    else {
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          val z = Library.isolate_substring(x)
+          if (z.length > max_string) z else store(z)
+      }
+    }
+  }
+
+  // main methods
+  def int(x: Int): Int = synchronized { cache_int(x) }
+  def string(x: String): String = synchronized { cache_string(x) }
+}

--- a/src/Pure/PIDE/xml.scala	Thu May 24 16:56:14 2018 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu May 24 21:13:09 2018 +0200
@@ -7,11 +7,6 @@
 package isabelle
 
 
-import java.util.{Collections, WeakHashMap}
-import java.lang.ref.WeakReference
-import javax.xml.parsers.DocumentBuilderFactory
-
-
 object XML
 {
   /** XML trees **/
@@ -152,55 +147,26 @@
 
 
 
-  /** cache for partial sharing (weak table) **/
+  /** cache **/
 
   def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
     new Cache(initial_size, max_string)
 
   class Cache private[XML](initial_size: Int, max_string: Int)
+    extends isabelle.Cache(initial_size, max_string)
   {
-    private val table =
-      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
-
-    def size: Int = table.size
-
-    private def lookup[A](x: A): Option[A] =
-    {
-      val ref = table.get(x)
-      if (ref == null) None
-      else {
-        val y = ref.asInstanceOf[WeakReference[A]].get
-        if (y == null) None
-        else Some(y)
-      }
-    }
-    private def store[A](x: A): A =
+    protected def cache_props(x: Properties.T): Properties.T =
     {
-      table.put(x, new WeakReference[Any](x))
-      x
-    }
-
-    private def cache_string(x: String): String =
-      if (x == "") ""
-      else if (x == "true") "true"
-      else if (x == "false") "false"
-      else if (x == "0.0") "0.0"
-      else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
-      else
-        lookup(x) match {
-          case Some(y) => y
-          case None =>
-            val z = Library.isolate_substring(x)
-            if (z.length > max_string) z else store(z)
-        }
-    private def cache_props(x: Properties.T): Properties.T =
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
         }
-    private def cache_markup(x: Markup): Markup =
+    }
+
+    protected def cache_markup(x: Markup): Markup =
+    {
       lookup(x) match {
         case Some(y) => y
         case None =>
@@ -209,7 +175,10 @@
               store(Markup(cache_string(name), cache_props(props)))
           }
       }
-    private def cache_tree(x: XML.Tree): XML.Tree =
+    }
+
+    protected def cache_tree(x: XML.Tree): XML.Tree =
+    {
       lookup(x) match {
         case Some(y) => y
         case None =>
@@ -219,16 +188,19 @@
             case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
-    private def cache_body(x: XML.Body): XML.Body =
+    }
+
+    protected def cache_body(x: XML.Body): XML.Body =
+    {
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
           case None => x.map(cache_tree(_))
         }
+    }
 
     // main methods
-    def string(x: String): String = synchronized { cache_string(x) }
     def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
     def markup(x: Markup): Markup = synchronized { cache_markup(x) }
     def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }

--- a/src/Pure/build-jars	Thu May 24 16:56:14 2018 +0200
+++ b/src/Pure/build-jars	Thu May 24 21:13:09 2018 +0200
@@ -41,6 +41,7 @@
   GUI/wrap_panel.scala
   General/antiquote.scala
   General/bytes.scala
+  General/cache.scala
   General/codepoint.scala
   General/comment.scala
   General/completion.scala

--- a/src/Pure/term.scala	Thu May 24 16:56:14 2018 +0200
+++ b/src/Pure/term.scala	Thu May 24 21:13:09 2018 +0200
@@ -29,5 +29,63 @@
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
+
+
+
+  /** cache **/
+
+  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
+    new Cache(initial_size, max_string)
+
+  class Cache private[Term](initial_size: Int, max_string: Int)
+    extends isabelle.Cache(initial_size, max_string)
+  {
+    protected def cache_indexname(x: Indexname): Indexname =
+      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
+
+    protected def cache_sort(x: Sort): Sort =
+      if (x == dummyS) dummyS
+      else lookup(x) getOrElse store(x.map(cache_string(_)))
+
+    protected def cache_typ(x: Typ): Typ =
+    {
+      if (x == dummyT) dummyT
+      else
+        lookup(x) match {
+          case Some(y) => y
+          case None =>
+            x match {
+              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
+              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
+              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
+            }
+        }
+    }
+
+    protected def cache_term(x: Term): Term =
+    {
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          x match {
+            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
+            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
+            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
+            case Bound(index) => store(Bound(cache_int(index)))
+            case Abs(name, typ, body) =>
+              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
+            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
+          }
+      }
+    }
+
+    // main methods
+    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
+    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
+    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
+    def term(x: Term): Term = synchronized { cache_term(x) }
+
+    def position(x: Position.T): Position.T =
+      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
+  }
 }
-