1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/html.scala	Fri Dec 04 22:51:59 2009 +0100
     1.3 @@ -0,0 +1,41 @@
     1.4 +/*  Title:      Pure/Thy/html.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Basic HTML output.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +object HTML
    1.13 +{
    1.14 +  // common elements and attributes
    1.15 +
    1.16 +  val BODY = "body"
    1.17 +  val DIV = "div"
    1.18 +  val SPAN = "span"
    1.19 +  val BR = "br"
    1.20 +  val CLASS = "class"
    1.21 +
    1.22 +
    1.23 +  // document markup
    1.24 +
    1.25 +  def body(trees: List[XML.Tree]): XML.Tree =
    1.26 +    XML.Elem(BODY, Nil, trees)
    1.27 +
    1.28 +  def div(trees: List[XML.Tree]): XML.Tree =
    1.29 +    XML.Elem(DIV, Nil, trees)
    1.30 +
    1.31 +  val br: XML.Tree = XML.Elem(BR, Nil, Nil)
    1.32 +
    1.33 +  def spans(tree: XML.Tree): List[XML.Tree] =
    1.34 +    tree match {
    1.35 +      case XML.Elem(name, _, ts) =>
    1.36 +        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
    1.37 +      case text @ XML.Text(txt) =>
    1.38 +        txt.split("\n").toList match {
    1.39 +          case line :: lines if !lines.isEmpty =>
    1.40 +            XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
    1.41 +          case _ => List(text)
    1.42 +        }
    1.43 +    }
    1.44 +}