wneuper/isa: src/Pure/Thy/html.scala@d163f0f28e8c

     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"

    42   // document markup

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

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

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

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

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

    53   def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =

    54   {

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

    56       tree match {

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

    58           if (original_data)

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

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

    61         case XML.Text(txt) =>

    62           val ts = new ListBuffer[XML.Tree]

    63           val t = new StringBuilder

    64           def flush() {

    65             if (!t.isEmpty) {

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

    67               t.clear

    68             }

    69           }

    70           def add(elem: XML.Tree) {

    71             flush()

    72             ts += elem

    73           }

    74           val syms = Symbol.iterator(txt).map(_.toString)

    75           while (syms.hasNext) {

    76             val s1 = syms.next

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

    78             s1 match {

    79               case "\n" => add(XML.elem(BR))

    80               case "\\<^bsub>" => t ++= s1  // FIXME

    81               case "\\<^esub>" => t ++= s1  // FIXME

    82               case "\\<^bsup>" => t ++= s1  // FIXME

    83               case "\\<^esup>" => t ++= s1  // FIXME

    84               case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))

    85               case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))

    86               case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))

    87               case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))

    88               case _ => t ++= s1

    89             }

    90           }

    91           flush()

    92           ts.toList

    93       }

    94     html_spans(input)

    95   }

    96 }

author	wenzelm
	Sun, 22 Aug 2010 13:52:24 +0200
changeset 38867	d163f0f28e8c
parent 38690	796904799f4d
child 44330	4b4b93672f15
permissions	-rw-r--r--