more readable output: whitespace is insignificant in HTML;
authorwenzelm
Sun Oct 23 16:44:17 2016 +0200 (2016-10-23)
changeset 643628a0fe5469ba0
parent 64361 07d910a58a14
child 64363 90ceace1e814
child 64364 464420ba7f74
child 64366 e0ab4c0a5a93
more readable output: whitespace is insignificant in HTML;
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Thy/html.scala	Sun Oct 23 16:37:59 2016 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Oct 23 16:44:17 2016 +0200
     1.3 @@ -69,9 +69,9 @@
     1.4          case XML.Elem(markup, Nil) =>
     1.5            s ++= "<"; elem(markup); s ++= "/>"
     1.6          case XML.Elem(markup, ts) =>
     1.7 -          s ++= "<"; elem(markup); s ++= ">"
     1.8 +          s ++= "\n<"; elem(markup); s ++= ">"
     1.9            ts.foreach(tree)
    1.10 -          s ++= "</"; s ++= markup.name; s ++= ">"
    1.11 +          s ++= "</"; s ++= markup.name; s ++= ">\n"
    1.12          case XML.Text(txt) => output(txt, s)
    1.13        }
    1.14      body.foreach(tree)