wneuper/isa: src/Pure/Thy/html.scala@0f3edc64356a

     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: List[XML.Tree]): XML.Elem =

    45     XML.Elem(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(tree: XML.Tree): List[XML.Tree] =

    54     tree match {

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

    56         List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))

    57       case XML.Text(txt) =>

    58         val ts = new ListBuffer[XML.Tree]

    59         val t = new StringBuilder

    60         def flush() {

    61           if (!t.isEmpty) {

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

    63             t.clear

    64           }

    65         }

    66         def add(elem: XML.Tree) {

    67           flush()

    68           ts += elem

    69         }

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

    71         while (syms.hasNext) {

    72           val s1 = syms.next

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

    74           s1 match {

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

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

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

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

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

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

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

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

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

    84             case _ => t ++= s1

    85           }

    86         }

    87         flush()

    88         ts.toList

    89     }

    90 }

author	wenzelm
	Sun, 30 May 2010 23:40:24 +0200
changeset 37201	0f3edc64356a
parent 36040	4f5c7a19ebe0
child 38486	ed147003de4b
permissions	-rw-r--r--