# HG changeset patch
# User wenzelm
# Date 1494787011 -7200
# Node ID 67a6e0f166c2449f15652bd09541f5bd8a88598e
# Parent  95fd3b9888e6ba40453c27bbe1250a3c2a16b89f
extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);

diff -r 95fd3b9888e6 -r 67a6e0f166c2 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun May 14 20:22:54 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 14 20:36:51 2017 +0200
@@ -58,6 +58,10 @@
 
   /* output XML as HTML */
 
+  private val structural_elements =
+    Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
+      "ul", "ol", "dl", "li", "dt", "dd")
+
   def output(body: XML.Body, s: StringBuilder)
   {
     def attrib(p: (String, String)): Unit =
@@ -69,9 +73,11 @@
         case XML.Elem(markup, Nil) =>
           s ++= "<"; elem(markup); s ++= "/>"
         case XML.Elem(markup, ts) =>
-          s ++= "\n<"; elem(markup); s ++= ">"
+          if (structural_elements(markup.name)) s += '\n'
+          s ++= "<"; elem(markup); s ++= ">"
           ts.foreach(tree)
-          s ++= "</"; s ++= markup.name; s ++= ">\n"
+          s ++= "</"; s ++= markup.name; s ++= ">"
+          if (structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) => output(txt, s)
       }
     body.foreach(tree)