src/Pure/Thy/html.scala
author wenzelm
Sat Aug 07 22:09:52 2010 +0200 (2010-08-07 ago)
changeset 38230 ed147003de4b
parent 37200 0f3edc64356a
child 38231 968844caaff9
permissions -rw-r--r--
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;
     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 
    41 
    42   // document markup
    43 
    44   def span(cls: String, body: List[XML.Tree]): XML.Elem =
    45     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    46 
    47   def hidden(txt: String): XML.Elem =
    48     span(Markup.HIDDEN, List(XML.Text(txt)))
    49 
    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)))
    52 
    53   def spans(tree: XML.Tree): List[XML.Tree] =
    54     tree match {
    55       case XML.Elem(Markup(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 }