# HG changeset patch
# User wenzelm
# Date 1612029536 -3600
# Node ID e2c25ea2ccf1dc98dd4db524810c2ba9109de241
# Parent  aa3d4cf7825a593c9683c3d4e6b159d0fabd91fa
tuned;

diff -r aa3d4cf7825a -r e2c25ea2ccf1 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Jan 30 18:34:37 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 18:58:56 2021 +0100
@@ -83,22 +83,24 @@
     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
       "ul", "ol", "dl", "li", "dt", "dd")
 
-  def output(s: StringBuilder, body: XML.Body, hidden: Boolean, structural: Boolean)
+  def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean)
   {
-    def tree(t: XML.Tree): Unit =
-      t match {
+    def output_body(body: XML.Body): Unit =
+    {
+      body foreach {
         case XML.Elem(markup, Nil) =>
           XML.output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
           XML.output_elem(s, markup)
-          ts.foreach(tree)
+          output_body(ts)
           XML.output_elem_end(s, markup.name)
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
           output(s, txt, hidden = hidden, permissive = true)
       }
-    body.foreach(tree)
+    }
+    output_body(xml)
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =