persistent hash code: much faster caching;

--- a/src/Pure/PIDE/xml.scala	Sat Jan 02 22:22:34 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 02 22:40:06 2021 +0100
@@ -20,6 +20,9 @@
   type Body = List[Tree]
   case class Elem(markup: Markup, body: Body) extends Tree
   {
+    private lazy val hash: Int = (markup, body).hashCode()
+    override def hashCode(): Int = hash
+
     def name: String = markup.name
 
     def update_attributes(more_attributes: Attributes): Elem =
@@ -29,6 +32,10 @@
     def + (att: Attribute): Elem = Elem(markup + att, body)
   }
   case class Text(content: String) extends Tree
+  {
+    private lazy val hash: Int = content.hashCode()
+    override def hashCode(): Int = hash
+  }
 
   def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
   def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)