# HG changeset patch
# User wenzelm
# Date 1496311024 -7200
# Node ID 868089ee9d60227c8239957382096fb3c26cc489
# Parent  68cd15585f4641b4e2837231146b9fba663b7fcc
uniform output of HTML as XML;
discontinued special cases of 041dc6d8d344;

diff -r 68cd15585f46 -r 868089ee9d60 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Wed May 31 21:48:32 2017 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 01 11:57:04 2017 +0200
@@ -93,23 +93,29 @@
 
   /** string representation **/
 
+  def output_char(c: Char, s: StringBuilder)
+  {
+    c match {
+      case '<' => s ++= "&lt;"
+      case '>' => s ++= "&gt;"
+      case '&' => s ++= "&amp;"
+      case '"' => s ++= "&quot;"
+      case '\'' => s ++= "&apos;"
+      case _ => s += c
+    }
+  }
+
+  def output_string(str: String, s: StringBuilder)
+  {
+    if (str == null) s ++= str
+    else str.iterator.foreach(c => output_char(c, s))
+  }
+
   def string_of_body(body: Body): String =
   {
     val s = new StringBuilder
 
-    def text(txt: String) {
-      if (txt == null) s ++= txt
-      else {
-        for (c <- txt.iterator) c match {
-          case '<' => s ++= "&lt;"
-          case '>' => s ++= "&gt;"
-          case '&' => s ++= "&amp;"
-          case '"' => s ++= "&quot;"
-          case '\'' => s ++= "&apos;"
-          case _ => s += c
-        }
-      }
-    }
+    def text(txt: String) { output_string(txt, s) }
     def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
     def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
     def tree(t: Tree): Unit =
diff -r 68cd15585f46 -r 868089ee9d60 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed May 31 21:48:32 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 01 11:57:04 2017 +0200
@@ -22,17 +22,7 @@
 
   def output(text: String, s: StringBuilder)
   {
-    def output_char(c: Char) =
-      c match {
-        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(str: String) = str.iterator.foreach(output_char(_))
+    def output_string(str: String) = XML.output_string(str, s)
 
     var ctrl = ""
     for (sym <- Symbol.iterator(text)) {
@@ -41,16 +31,16 @@
         control.get(ctrl) match {
           case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
             s ++= ("<" + elem + ">")
-            output_chars(sym)
+            output_string(sym)
             s ++= ("</" + elem + ">")
           case _ =>
-            output_chars(ctrl)
-            output_chars(sym)
+            output_string(ctrl)
+            output_string(sym)
         }
         ctrl = ""
       }
     }
-    output_chars(ctrl)
+    output_string(ctrl)
   }
 
   def output(text: String): String = Library.make_string(output(text, _))