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 =