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.
     1 /*  Title:      Pure/Thy/html.scala
     2     Author:     Makarius
     3 
     4 Basic HTML output.
     5 */
     6 
     7 package isabelle
     8 
     9 object HTML
    10 {
    11   // common elements and attributes
    12 
    13   val BODY = "body"
    14   val DIV = "div"
    15   val SPAN = "span"
    16   val BR = "br"
    17   val CLASS = "class"
    18 
    19 
    20   // document markup
    21 
    22   def body(trees: List[XML.Tree]): XML.Tree =
    23     XML.Elem(BODY, Nil, trees)
    24 
    25   def div(trees: List[XML.Tree]): XML.Tree =
    26     XML.Elem(DIV, Nil, trees)
    27 
    28   val br: XML.Tree = XML.Elem(BR, Nil, Nil)
    29 
    30   def spans(tree: XML.Tree): List[XML.Tree] =
    31     tree match {
    32       case XML.Elem(name, _, ts) =>
    33         List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
    34       case text @ XML.Text(txt) =>
    35         txt.split("\n").toList match {
    36           case line :: lines if !lines.isEmpty =>
    37             XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
    38           case _ => List(text)
    39         }
    40     }
    41 }