# HG changeset patch
# User wenzelm
# Date 1496697188 -7200
# Node ID 9ce3720976dc5f84a801df0ca67262f1c2be08e3
# Parent  57acac0fd29b03e57595e7c5b4a75d0856a98fe5
permissive output of XML.Text, e.g. relevant for embedded <style>;

diff -r 57acac0fd29b -r 9ce3720976dc src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Jun 05 15:59:47 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon Jun 05 23:13:08 2017 +0200
@@ -26,8 +26,25 @@
 
   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
 
-  def output(text: String, s: StringBuilder, hidden: Boolean)
+  def output_char_permissive(c: Char, s: StringBuilder)
   {
+    c match {
+      case '<' => s ++= "&lt;"
+      case '>' => s ++= "&gt;"
+      case '&' => s ++= "&amp;"
+      case _ => s += c
+    }
+  }
+
+  def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean)
+  {
+    def output_char(c: Char): Unit =
+      if (permissive) output_char_permissive(c, s)
+      else XML.output_char(c, s)
+
+    def output_string(str: String): Unit =
+      str.iterator.foreach(output_char)
+
     def output_hidden(body: => Unit): Unit =
       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
 
@@ -35,11 +52,11 @@
       if (sym != "") {
         control_block.get(sym) match {
           case Some(html) if html.startsWith("</") =>
-            s ++= html; output_hidden(XML.output_string(sym, s))
+            s ++= html; output_hidden(output_string(sym))
           case Some(html) =>
-            output_hidden(XML.output_string(sym, s)); s ++= html
+            output_hidden(output_string(sym)); s ++= html
           case None =>
-            XML.output_string(sym, s)
+            output_string(sym)
         }
       }
 
@@ -63,7 +80,8 @@
     output_symbol(ctrl)
   }
 
-  def output(text: String): String = Library.make_string(output(text, _, hidden = false))
+  def output(text: String): String =
+    Library.make_string(output(text, _, hidden = false, permissive = true))
 
 
   /* output XML as HTML */
@@ -78,7 +96,12 @@
     {
       s ++= markup.name
       for ((a, b) <- markup.properties) {
-        s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"'
+        s += ' '
+        s ++= a
+        s += '='
+        s += '"'
+        output(b, s, hidden = hidden, permissive = false)
+        s += '"'
       }
     }
     def tree(t: XML.Tree): Unit =
@@ -92,7 +115,7 @@
           s ++= "</"; s ++= markup.name; s += '>'
           if (structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
-          output(txt, s, hidden)
+          output(txt, s, hidden = hidden, permissive = true)
       }
     body.foreach(tree)
   }