# HG changeset patch
# User wenzelm
# Date 1477218657 -7200
# Node ID c6a1031cf9253ef98be20d1ef266f7341610d4ce
# Parent  d9c7a8e83c3d917b2a17d57dce6f5ed97539b921
support for XML as HTML;
tuned;

diff -r d9c7a8e83c3d -r c6a1031cf925 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Oct 23 12:27:11 2016 +0200
+++ b/src/Pure/Thy/html.scala	Sun Oct 23 12:30:57 2016 +0200
@@ -20,21 +20,19 @@
       Symbol.bold -> "b",
       Symbol.bold_decoded -> "b")
 
-  def output(text: String): String =
+  def output(text: String, s: StringBuilder)
   {
-    val result = new StringBuilder
-
     def output_char(c: Char) =
       c match {
-        case '<' => result ++= "&lt;"
-        case '>' => result ++= "&gt;"
-        case '&' => result ++= "&amp;"
-        case '"' => result ++= "&quot;"
-        case '\'' => result ++= "&#39;"
-        case '\n' => result ++= "<br/>"
-        case _ => result += c
+        case '<' => s ++= "&lt;"
+        case '>' => s ++= "&gt;"
+        case '&' => s ++= "&amp;"
+        case '"' => s ++= "&quot;"
+        case '\'' => s ++= "&#39;"
+        case '\n' => s ++= "<br/>"
+        case _ => s += c
       }
-    def output_chars(s: String) = s.iterator.foreach(output_char(_))
+    def output_chars(str: String) = str.iterator.foreach(output_char(_))
 
     var ctrl = ""
     for (sym <- Symbol.iterator(text)) {
@@ -42,9 +40,9 @@
       else {
         control.get(ctrl) match {
           case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
-            result ++= ("<" + elem + ">")
+            s ++= ("<" + elem + ">")
             output_chars(sym)
-            result ++= ("</" + elem + ">")
+            s ++= ("</" + elem + ">")
           case _ =>
             output_chars(ctrl)
             output_chars(sym)
@@ -53,10 +51,45 @@
       }
     }
     output_chars(ctrl)
+  }
 
-    result.toString
+  def output(text: String): String = Library.make_string(output(text, _))
+
+
+  /* output XML as HTML */
+
+  def output(body: XML.Body, s: StringBuilder)
+  {
+    def attrib(p: (String, String)): Unit =
+      { s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
+    def elem(markup: Markup): Unit =
+      { s ++= markup.name; markup.properties.foreach(attrib) }
+    def tree(t: XML.Tree): Unit =
+      t match {
+        case XML.Elem(markup, Nil) =>
+          s ++= "<"; elem(markup); s ++= "/>"
+        case XML.Elem(markup, ts) =>
+          s ++= "<"; elem(markup); s ++= ">"
+          ts.foreach(tree)
+          s ++= "</"; s ++= markup.name; s ++= ">"
+        case XML.Text(txt) => output(txt, s)
+      }
+    body.foreach(tree)
   }
 
+  def output(body: XML.Body): String = Library.make_string(output(body, _))
+  def output(tree: XML.Tree): String = output(List(tree))
+
+
+  /* structured markup */
+
+  def chapter(body: XML.Body): XML.Elem = XML.elem("h1", body)
+  def section(body: XML.Body): XML.Elem = XML.elem("h2", body)
+  def subsection(body: XML.Body): XML.Elem = XML.elem("h3", body)
+  def subsubsection(body: XML.Body): XML.Elem = XML.elem("h4", body)
+  def paragraph(body: XML.Body): XML.Elem = XML.elem("h5", body)
+  def subparagraph(body: XML.Body): XML.Elem = XML.elem("h6", body)
+
 
   /* document */
 
diff -r d9c7a8e83c3d -r c6a1031cf925 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Oct 23 12:27:11 2016 +0200
+++ b/src/Pure/library.scala	Sun Oct 23 12:30:57 2016 +0200
@@ -119,6 +119,13 @@
 
   /* strings */
 
+  def make_string(f: StringBuilder => Unit): String =
+  {
+    val s = new StringBuilder
+    f(s)
+    s.toString
+  }
+
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None