src/Pure/Thy/html.scala
author wenzelm
Fri Dec 04 22:51:59 2009 +0100 (2009-12-04 ago)
changeset 33984 c54498f88a77
child 34000 1fecda948697
permissions -rw-r--r--
Basic HTML output.
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@33984
     9
object HTML
wenzelm@33984
    10
{
wenzelm@33984
    11
  // common elements and attributes
wenzelm@33984
    12
wenzelm@33984
    13
  val BODY = "body"
wenzelm@33984
    14
  val DIV = "div"
wenzelm@33984
    15
  val SPAN = "span"
wenzelm@33984
    16
  val BR = "br"
wenzelm@33984
    17
  val CLASS = "class"
wenzelm@33984
    18
wenzelm@33984
    19
wenzelm@33984
    20
  // document markup
wenzelm@33984
    21
wenzelm@33984
    22
  def body(trees: List[XML.Tree]): XML.Tree =
wenzelm@33984
    23
    XML.Elem(BODY, Nil, trees)
wenzelm@33984
    24
wenzelm@33984
    25
  def div(trees: List[XML.Tree]): XML.Tree =
wenzelm@33984
    26
    XML.Elem(DIV, Nil, trees)
wenzelm@33984
    27
wenzelm@33984
    28
  val br: XML.Tree = XML.Elem(BR, Nil, Nil)
wenzelm@33984
    29
wenzelm@33984
    30
  def spans(tree: XML.Tree): List[XML.Tree] =
wenzelm@33984
    31
    tree match {
wenzelm@33984
    32
      case XML.Elem(name, _, ts) =>
wenzelm@33984
    33
        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
wenzelm@33984
    34
      case text @ XML.Text(txt) =>
wenzelm@33984
    35
        txt.split("\n").toList match {
wenzelm@33984
    36
          case line :: lines if !lines.isEmpty =>
wenzelm@33984
    37
            XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
wenzelm@33984
    38
          case _ => List(text)
wenzelm@33984
    39
        }
wenzelm@33984
    40
    }
wenzelm@33984
    41
}