# HG changeset patch
# User wenzelm
# Date 1612023314 -3600
# Node ID 9c10b4fa17b531f6adeb7cfc326fcd87a82f7ddb
# Parent  8a17c7bf530af722129d4b7e179edc4753fc4db4
clarified signature;

diff -r 8a17c7bf530a -r 9c10b4fa17b5 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Jan 30 17:06:13 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 30 17:15:14 2021 +0100
@@ -128,22 +128,22 @@
 
   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
 
-  def output_char(s: StringBuilder, c: Char)
+  def output_char(s: StringBuilder, c: Char, permissive: Boolean = false)
   {
     c match {
       case '<' => s ++= "&lt;"
       case '>' => s ++= "&gt;"
       case '&' => s ++= "&amp;"
-      case '"' => s ++= "&quot;"
-      case '\'' => s ++= "&apos;"
+      case '"' if !permissive => s ++= "&quot;"
+      case '\'' if !permissive => s ++= "&apos;"
       case _ => s += c
     }
   }
 
-  def output_string(s: StringBuilder, str: String)
+  def output_string(s: StringBuilder, str: String, permissive: Boolean = false)
   {
     if (str == null) s ++= str
-    else str.iterator.foreach(c => output_char(s, c))
+    else str.iterator.foreach(output_char(s, _, permissive = permissive))
   }
 
   def string_of_body(body: Body): String =
diff -r 8a17c7bf530a -r 9c10b4fa17b5 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Jan 30 17:06:13 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 17:15:14 2021 +0100
@@ -26,21 +26,10 @@
 
   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
 
-  def output_char_permissive(s: StringBuilder, c: Char)
-  {
-    c match {
-      case '<' => s ++= "&lt;"
-      case '>' => s ++= "&gt;"
-      case '&' => s ++= "&amp;"
-      case _ => s += c
-    }
-  }
-
   def output(s: StringBuilder, text: String, hidden: Boolean, permissive: Boolean)
   {
     def output_char(c: Char): Unit =
-      if (permissive) output_char_permissive(s, c)
-      else XML.output_char(s, c)
+      XML.output_char(s, c, permissive = permissive)
 
     def output_string(str: String): Unit =
       str.iterator.foreach(output_char)