src/Pure/Thy/html.scala
changeset 73204 aa3d4cf7825a
parent 73203 9c10b4fa17b5
child 73205 e2c25ea2ccf1
equal deleted inserted replaced
73203:9c10b4fa17b5 73204:aa3d4cf7825a
    26 
    26 
    27   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
    27   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
    28 
    28 
    29   def output(s: StringBuilder, text: String, hidden: Boolean, permissive: Boolean)
    29   def output(s: StringBuilder, text: String, hidden: Boolean, permissive: Boolean)
    30   {
    30   {
    31     def output_char(c: Char): Unit =
       
    32       XML.output_char(s, c, permissive = permissive)
       
    33 
       
    34     def output_string(str: String): Unit =
    31     def output_string(str: String): Unit =
    35       str.iterator.foreach(output_char)
    32       XML.output_string(s, str, permissive = permissive)
    36 
    33 
    37     def output_hidden(body: => Unit): Unit =
    34     def output_hidden(body: => Unit): Unit =
    38       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
    35       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
    39 
    36 
    40     def output_symbol(sym: Symbol.Symbol): Unit =
    37     def output_symbol(sym: Symbol.Symbol): Unit =
    61       if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
    58       if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
    62       else {
    59       else {
    63         control.get(ctrl) match {
    60         control.get(ctrl) match {
    64           case Some(elem) if Symbol.is_controllable(sym) =>
    61           case Some(elem) if Symbol.is_controllable(sym) =>
    65             output_hidden(output_symbol(ctrl))
    62             output_hidden(output_symbol(ctrl))
    66             s += '<'; s ++= elem; s += '>'
    63             XML.output_elem(s, Markup(elem, Nil))
    67             output_symbol(sym)
    64             output_symbol(sym)
    68             s ++= "</"; s ++= elem; s += '>'
    65             XML.output_elem_end(s, elem)
    69           case _ =>
    66           case _ =>
    70             output_symbol(ctrl)
    67             output_symbol(ctrl)
    71             output_symbol(sym)
    68             output_symbol(sym)
    72         }
    69         }
    73         ctrl = ""
    70         ctrl = ""
    86     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
    83     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
    87       "ul", "ol", "dl", "li", "dt", "dd")
    84       "ul", "ol", "dl", "li", "dt", "dd")
    88 
    85 
    89   def output(s: StringBuilder, body: XML.Body, hidden: Boolean, structural: Boolean)
    86   def output(s: StringBuilder, body: XML.Body, hidden: Boolean, structural: Boolean)
    90   {
    87   {
    91     def elem(markup: Markup)
       
    92     {
       
    93       s ++= markup.name
       
    94       for ((a, b) <- markup.properties) {
       
    95         s += ' '
       
    96         s ++= a
       
    97         s += '='
       
    98         s += '"'
       
    99         output(s, b, hidden = hidden, permissive = false)
       
   100         s += '"'
       
   101       }
       
   102     }
       
   103     def tree(t: XML.Tree): Unit =
    88     def tree(t: XML.Tree): Unit =
   104       t match {
    89       t match {
   105         case XML.Elem(markup, Nil) =>
    90         case XML.Elem(markup, Nil) =>
   106           s += '<'; elem(markup); s ++= "/>"
    91           XML.output_elem(s, markup, end = true)
   107         case XML.Elem(markup, ts) =>
    92         case XML.Elem(markup, ts) =>
   108           if (structural && structural_elements(markup.name)) s += '\n'
    93           if (structural && structural_elements(markup.name)) s += '\n'
   109           s += '<'; elem(markup); s += '>'
    94           XML.output_elem(s, markup)
   110           ts.foreach(tree)
    95           ts.foreach(tree)
   111           s ++= "</"; s ++= markup.name; s += '>'
    96           XML.output_elem_end(s, markup.name)
   112           if (structural && structural_elements(markup.name)) s += '\n'
    97           if (structural && structural_elements(markup.name)) s += '\n'
   113         case XML.Text(txt) =>
    98         case XML.Text(txt) =>
   114           output(s, txt, hidden = hidden, permissive = true)
    99           output(s, txt, hidden = hidden, permissive = true)
   115       }
   100       }
   116     body.foreach(tree)
   101     body.foreach(tree)