# HG changeset patch
# User wenzelm
# Date 1609623606 -3600
# Node ID 72b13af7f26625b5d26716e4fe6795e634641dc3
# Parent  f93f0597f4fb2d4ff35962de90d1499c65d3e783
persistent hash code: much faster caching;

diff -r f93f0597f4fb -r 72b13af7f266 src/Pure/PIDE/xml.scala
--- 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)