wneuper/isa: src/Pure/Thy/html.scala@36120feb70ed

     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(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 span_class =

    64             m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }

    65           val html_span = span(span_class, ts.flatMap(html_spans))

    66           if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))

    67           else List(html_span)

    68         case XML.Text(txt) =>

    69           val ts = new ListBuffer[XML.Tree]

    70           val t = new StringBuilder

    71           def flush() {

    72             if (!t.isEmpty) {

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

    74               t.clear

    75             }

    76           }

    77           def add(elem: XML.Tree) {

    78             flush()

    79             ts += elem

    80           }

    81           val syms = Symbol.iterator(txt)

    82           while (syms.hasNext) {

    83             val s1 = syms.next

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

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

    86             else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)

    87               { add(hidden(s1)); add(sub(s2())) }

    88             else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)

    89               { add(hidden(s1)); add(sup(s2())) }

    90             else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME

    91             else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME

    92             else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME

    93             else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME

    94             else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }

    95             else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }

    96             else t ++= s1

    97           }

    98           flush()

    99           ts.toList

   100       }

   101     html_spans(input)

   102   }

   103 }

author	wenzelm
	Wed, 17 Aug 2011 16:01:27 +0200
changeset 45109	36120feb70ed
parent 44569	5130dfe1b7be
child 46537	d83797ef0d2d
permissions	-rw-r--r--