# HG changeset patch
# User wenzelm
# Date 1477233857 -7200
# Node ID 8a0fe5469ba08e00d729cef19c57f7408716f902
# Parent  07d910a58a14ab24d0ac0729448af73054c78940
more readable output: whitespace is insignificant in HTML;

diff -r 07d910a58a14 -r 8a0fe5469ba0 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Oct 23 16:37:59 2016 +0200
+++ b/src/Pure/Thy/html.scala	Sun Oct 23 16:44:17 2016 +0200
@@ -69,9 +69,9 @@
         case XML.Elem(markup, Nil) =>
           s ++= "<"; elem(markup); s ++= "/>"
         case XML.Elem(markup, ts) =>
-          s ++= "<"; elem(markup); s ++= ">"
+          s ++= "\n<"; elem(markup); s ++= ">"
           ts.foreach(tree)
-          s ++= "</"; s ++= markup.name; s ++= ">"
+          s ++= "</"; s ++= markup.name; s ++= ">\n"
         case XML.Text(txt) => output(txt, s)
       }
     body.foreach(tree)