src/Pure/Thy/html.scala
author wenzelm
Sat Mar 10 23:28:42 2012 +0100 (2012-03-10 ago)
changeset 46865 659dcbafe4bf
parent 45666 d83797ef0d2d
child 49613 2f6986e2ef06
permissions -rw-r--r--
discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
uniform treatment of "class" entities in input and output;
     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   val STYLE = "style"
    41 
    42 
    43   // document markup
    44 
    45   def span(cls: String, body: XML.Body): XML.Elem =
    46     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    47 
    48   def user_font(font: String, txt: String): XML.Elem =
    49     XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
    50 
    51   def hidden(txt: String): XML.Elem =
    52     span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
    53 
    54   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    55   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    56   def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
    57 
    58   def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
    59   {
    60     def html_spans(tree: XML.Tree): XML.Body =
    61       tree match {
    62         case XML.Elem(m @ Markup(name, props), ts) =>
    63           val html_span = span(name, ts.flatMap(html_spans))
    64           if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
    65           else List(html_span)
    66         case XML.Text(txt) =>
    67           val ts = new ListBuffer[XML.Tree]
    68           val t = new StringBuilder
    69           def flush() {
    70             if (!t.isEmpty) {
    71               ts += XML.Text(t.toString)
    72               t.clear
    73             }
    74           }
    75           def add(elem: XML.Tree) {
    76             flush()
    77             ts += elem
    78           }
    79           val syms = Symbol.iterator(txt)
    80           while (syms.hasNext) {
    81             val s1 = syms.next
    82             def s2() = if (syms.hasNext) syms.next else ""
    83             if (s1 == "\n") add(XML.elem(BR))
    84             else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
    85               { add(hidden(s1)); add(sub(s2())) }
    86             else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
    87               { add(hidden(s1)); add(sup(s2())) }
    88             else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
    89             else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
    90             else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
    91             else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
    92             else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
    93             else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
    94             else t ++= s1
    95           }
    96           flush()
    97           ts.toList
    98       }
    99     html_spans(input)
   100   }
   101 }