src/Pure/Thy/html.scala
author wenzelm
Sun Dec 06 22:23:31 2009 +0100 (2009-12-06 ago)
changeset 34000 1fecda948697
parent 33984 c54498f88a77
child 34002 cbeeef3aebb3
permissions -rw-r--r--
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm@33984
     1
/*  Title:      Pure/Thy/html.scala
wenzelm@33984
     2
    Author:     Makarius
wenzelm@33984
     3
wenzelm@33984
     4
Basic HTML output.
wenzelm@33984
     5
*/
wenzelm@33984
     6
wenzelm@33984
     7
package isabelle
wenzelm@33984
     8
wenzelm@34000
     9
import scala.collection.mutable.ListBuffer
wenzelm@34000
    10
wenzelm@34000
    11
wenzelm@33984
    12
object HTML
wenzelm@33984
    13
{
wenzelm@33984
    14
  // common elements and attributes
wenzelm@33984
    15
wenzelm@33984
    16
  val BODY = "body"
wenzelm@33984
    17
  val DIV = "div"
wenzelm@33984
    18
  val SPAN = "span"
wenzelm@33984
    19
  val BR = "br"
wenzelm@34000
    20
  val PRE = "pre"
wenzelm@33984
    21
  val CLASS = "class"
wenzelm@33984
    22
wenzelm@33984
    23
wenzelm@33984
    24
  // document markup
wenzelm@33984
    25
wenzelm@33984
    26
  def spans(tree: XML.Tree): List[XML.Tree] =
wenzelm@33984
    27
    tree match {
wenzelm@33984
    28
      case XML.Elem(name, _, ts) =>
wenzelm@33984
    29
        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
wenzelm@34000
    30
      case XML.Text(txt) =>
wenzelm@34000
    31
        val ts = new ListBuffer[XML.Tree]
wenzelm@34000
    32
        val t = new StringBuilder
wenzelm@34000
    33
        def flush_text() {
wenzelm@34000
    34
          if (!t.isEmpty) {
wenzelm@34000
    35
            ts + XML.Text(t.toString)
wenzelm@34000
    36
            t.clear
wenzelm@34000
    37
          }
wenzelm@33984
    38
        }
wenzelm@34000
    39
        for (sym <- Symbol.elements(txt)) {
wenzelm@34000
    40
          sym match {
wenzelm@34000
    41
            case "\n" =>
wenzelm@34000
    42
              flush_text()
wenzelm@34000
    43
              ts + XML.elem(BR)
wenzelm@34000
    44
            case _ =>
wenzelm@34000
    45
              t ++ sym.toString
wenzelm@34000
    46
          }
wenzelm@34000
    47
        }
wenzelm@34000
    48
        flush_text()
wenzelm@34000
    49
        ts.toList
wenzelm@33984
    50
    }
wenzelm@33984
    51
}