src/Pure/Thy/html.scala
author wenzelm
Tue Jun 21 13:29:44 2011 +0200 (2011-06-21 ago)
changeset 43489 132f99cc0a43
parent 43459 def9784a3316
child 43490 5e6f76cacb93
permissions -rw-r--r--
tuned iteration over short symbols;
     1 /*  Title:      Pure/Thy/html.scala
     2     Author:     Makarius
     3 
     4 Basic HTML output.
     5 */
     6 
     7 package isabelle
     8 
     9 import scala.collection.mutable.ListBuffer
    10 
    11 
    12 object HTML
    13 {
    14   // encode text
    15 
    16   def encode(text: String): String =
    17   {
    18     val s = new StringBuilder
    19     for (c <- text.iterator) c match {
    20       case '<' => s ++= "&lt;"
    21       case '>' => s ++= "&gt;"
    22       case '&' => s ++= "&amp;"
    23       case '"' => s ++= "&quot;"
    24       case '\'' => s ++= "&#39;"
    25       case '\n' => s ++= "<br/>"
    26       case _ => s += c
    27     }
    28     s.toString
    29   }
    30 
    31 
    32   // common elements and attributes
    33 
    34   val BODY = "body"
    35   val DIV = "div"
    36   val SPAN = "span"
    37   val BR = "br"
    38   val PRE = "pre"
    39   val CLASS = "class"
    40 
    41 
    42   // document markup
    43 
    44   def span(cls: String, body: XML.Body): XML.Elem =
    45     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    46 
    47   def hidden(txt: String): XML.Elem =
    48     span(Markup.HIDDEN, List(XML.Text(txt)))
    49 
    50   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    51   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    52   def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
    53 
    54   def spans(symbols: Symbol.Interpretation,
    55     input: XML.Tree, original_data: Boolean = false): XML.Body =
    56   {
    57     def html_spans(tree: XML.Tree): XML.Body =
    58       tree match {
    59         case XML.Elem(Markup(name, _), ts) =>
    60           if (original_data)
    61             List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
    62           else List(span(name, ts.flatMap(html_spans)))
    63         case XML.Text(txt) =>
    64           val ts = new ListBuffer[XML.Tree]
    65           val t = new StringBuilder
    66           def flush() {
    67             if (!t.isEmpty) {
    68               ts += XML.Text(t.toString)
    69               t.clear
    70             }
    71           }
    72           def add(elem: XML.Tree) {
    73             flush()
    74             ts += elem
    75           }
    76           val syms = Symbol.iterator_string(txt)
    77           while (syms.hasNext) {
    78             val s1 = syms.next
    79             def s2() = if (syms.hasNext) syms.next else ""
    80             if (s1 == "\n") add(XML.elem(BR))
    81             else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
    82             else if (s1 == "\\<^esub>") t ++= s1  // FIXME
    83             else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
    84             else if (s1 == "\\<^esup>") t ++= s1  // FIXME
    85             else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    86             else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    87             else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    88             else t ++= s1
    89           }
    90           flush()
    91           ts.toList
    92       }
    93     html_spans(input)
    94   }
    95 }