src/Pure/PIDE/xml.scala
changeset 73203 9c10b4fa17b5
parent 73202 8a17c7bf530a
child 73204 aa3d4cf7825a
equal deleted inserted replaced
73202:8a17c7bf530a 73203:9c10b4fa17b5
   126 
   126 
   127   /** string representation **/
   127   /** string representation **/
   128 
   128 
   129   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
   129   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
   130 
   130 
   131   def output_char(s: StringBuilder, c: Char)
   131   def output_char(s: StringBuilder, c: Char, permissive: Boolean = false)
   132   {
   132   {
   133     c match {
   133     c match {
   134       case '<' => s ++= "&lt;"
   134       case '<' => s ++= "&lt;"
   135       case '>' => s ++= "&gt;"
   135       case '>' => s ++= "&gt;"
   136       case '&' => s ++= "&amp;"
   136       case '&' => s ++= "&amp;"
   137       case '"' => s ++= "&quot;"
   137       case '"' if !permissive => s ++= "&quot;"
   138       case '\'' => s ++= "&apos;"
   138       case '\'' if !permissive => s ++= "&apos;"
   139       case _ => s += c
   139       case _ => s += c
   140     }
   140     }
   141   }
   141   }
   142 
   142 
   143   def output_string(s: StringBuilder, str: String)
   143   def output_string(s: StringBuilder, str: String, permissive: Boolean = false)
   144   {
   144   {
   145     if (str == null) s ++= str
   145     if (str == null) s ++= str
   146     else str.iterator.foreach(c => output_char(s, c))
   146     else str.iterator.foreach(output_char(s, _, permissive = permissive))
   147   }
   147   }
   148 
   148 
   149   def string_of_body(body: Body): String =
   149   def string_of_body(body: Body): String =
   150   {
   150   {
   151     val s = new StringBuilder
   151     val s = new StringBuilder