wneuper/isa: src/Pure/Thy/html.scala@5e6f76cacb93

     1 /*  Title:      Pure/Thy/html.scala

     2     Author:     Makarius

     4 Basic HTML output.

     5 */

     7 package isabelle

     9 import scala.collection.mutable.ListBuffer

    12 object HTML

    13 {

    14   // encode text

    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   }

    32   // common elements and attributes

    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"

    43   // document markup

    45   def span(cls: String, body: XML.Body): XML.Elem =

    46     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)

    48   def user_font(font: String, txt: String): XML.Elem =

    49     XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))

    51   def hidden(txt: String): XML.Elem =

    52     span(Markup.HIDDEN, List(XML.Text(txt)))

    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)))

    58   def spans(symbols: Symbol.Interpretation,

    59     input: XML.Tree, original_data: Boolean = false): XML.Body =

    60   {

    61     def html_spans(tree: XML.Tree): XML.Body =

    62       tree match {

    63         case XML.Elem(Markup(name, _), ts) =>

    64           if (original_data)

    65             List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))

    66           else List(span(name, ts.flatMap(html_spans)))

    67         case XML.Text(txt) =>

    68           val ts = new ListBuffer[XML.Tree]

    69           val t = new StringBuilder

    70           def flush() {

    71             if (!t.isEmpty) {

    72               ts += XML.Text(t.toString)

    73               t.clear

    74             }

    75           }

    76           def add(elem: XML.Tree) {

    77             flush()

    78             ts += elem

    79           }

    80           val syms = Symbol.iterator_string(txt)

    81           while (syms.hasNext) {

    82             val s1 = syms.next

    83             def s2() = if (syms.hasNext) syms.next else ""

    84             if (s1 == "\n") add(XML.elem(BR))

    85             else if (s1 == "\\<^bsub>") t ++= s1  // FIXME

    86             else if (s1 == "\\<^esub>") t ++= s1  // FIXME

    87             else if (s1 == "\\<^bsup>") t ++= s1  // FIXME

    88             else if (s1 == "\\<^esup>") t ++= s1  // FIXME

    89             else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }

    90             else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }

    91             else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }

    92             else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }

    93             else t ++= s1

    94           }

    95           flush()

    96           ts.toList

    97       }

    98     html_spans(input)

    99   }

   100 }

author	wenzelm
	Tue, 21 Jun 2011 14:12:49 +0200
changeset 44361	5e6f76cacb93
parent 44360	132f99cc0a43
child 44382	d138e7482a1b
permissions	-rw-r--r--