permissive output of XML.Text, e.g. relevant for embedded <style>;
authorwenzelm
Mon Jun 05 23:13:08 2017 +0200 (2017-06-05)
changeset 660189ce3720976dc
parent 66017 57acac0fd29b
child 66019 69b5ef78fb07
permissive output of XML.Text, e.g. relevant for embedded <style>;
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Thy/html.scala	Mon Jun 05 15:59:47 2017 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Mon Jun 05 23:13:08 2017 +0200
     1.3 @@ -26,8 +26,25 @@
     1.4  
     1.5    def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
     1.6  
     1.7 -  def output(text: String, s: StringBuilder, hidden: Boolean)
     1.8 +  def output_char_permissive(c: Char, s: StringBuilder)
     1.9    {
    1.10 +    c match {
    1.11 +      case '<' => s ++= "&lt;"
    1.12 +      case '>' => s ++= "&gt;"
    1.13 +      case '&' => s ++= "&amp;"
    1.14 +      case _ => s += c
    1.15 +    }
    1.16 +  }
    1.17 +
    1.18 +  def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean)
    1.19 +  {
    1.20 +    def output_char(c: Char): Unit =
    1.21 +      if (permissive) output_char_permissive(c, s)
    1.22 +      else XML.output_char(c, s)
    1.23 +
    1.24 +    def output_string(str: String): Unit =
    1.25 +      str.iterator.foreach(output_char)
    1.26 +
    1.27      def output_hidden(body: => Unit): Unit =
    1.28        if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
    1.29  
    1.30 @@ -35,11 +52,11 @@
    1.31        if (sym != "") {
    1.32          control_block.get(sym) match {
    1.33            case Some(html) if html.startsWith("</") =>
    1.34 -            s ++= html; output_hidden(XML.output_string(sym, s))
    1.35 +            s ++= html; output_hidden(output_string(sym))
    1.36            case Some(html) =>
    1.37 -            output_hidden(XML.output_string(sym, s)); s ++= html
    1.38 +            output_hidden(output_string(sym)); s ++= html
    1.39            case None =>
    1.40 -            XML.output_string(sym, s)
    1.41 +            output_string(sym)
    1.42          }
    1.43        }
    1.44  
    1.45 @@ -63,7 +80,8 @@
    1.46      output_symbol(ctrl)
    1.47    }
    1.48  
    1.49 -  def output(text: String): String = Library.make_string(output(text, _, hidden = false))
    1.50 +  def output(text: String): String =
    1.51 +    Library.make_string(output(text, _, hidden = false, permissive = true))
    1.52  
    1.53  
    1.54    /* output XML as HTML */
    1.55 @@ -78,7 +96,12 @@
    1.56      {
    1.57        s ++= markup.name
    1.58        for ((a, b) <- markup.properties) {
    1.59 -        s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"'
    1.60 +        s += ' '
    1.61 +        s ++= a
    1.62 +        s += '='
    1.63 +        s += '"'
    1.64 +        output(b, s, hidden = hidden, permissive = false)
    1.65 +        s += '"'
    1.66        }
    1.67      }
    1.68      def tree(t: XML.Tree): Unit =
    1.69 @@ -92,7 +115,7 @@
    1.70            s ++= "</"; s ++= markup.name; s += '>'
    1.71            if (structural_elements(markup.name)) s += '\n'
    1.72          case XML.Text(txt) =>
    1.73 -          output(txt, s, hidden)
    1.74 +          output(txt, s, hidden = hidden, permissive = true)
    1.75        }
    1.76      body.foreach(tree)
    1.77    }