author | wenzelm |
Sun, 23 Oct 2016 16:44:17 +0200 | |
changeset 64362 | 8a0fe5469ba0 |
parent 64361 | 07d910a58a14 |
child 64363 | 90ceace1e814 |
child 64364 | 464420ba7f74 |
child 64366 | e0ab4c0a5a93 |
--- 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)