extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);

--- 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)