1.1 --- a/src/Pure/IsaMakefile	Fri Dec 04 20:03:37 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Fri Dec 04 22:51:59 2009 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4    System/cygwin.scala System/gui_setup.scala				\
     1.5    System/isabelle_process.scala System/isabelle_syntax.scala		\
     1.6    System/isabelle_system.scala System/platform.scala			\
     1.7 -  Thy/completion.scala Thy/thy_header.scala
     1.8 +  Thy/completion.scala Thy/html.scala Thy/thy_header.scala
     1.9  
    1.10  JAR_DIR = $(ISABELLE_HOME)/lib/classes
    1.11  PURE_JAR = $(JAR_DIR)/Pure.jar

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Thy/html.scala	Fri Dec 04 22:51:59 2009 +0100
     2.3 @@ -0,0 +1,41 @@
     2.4 +/*  Title:      Pure/Thy/html.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Basic HTML output.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +object HTML
    2.13 +{
    2.14 +  // common elements and attributes
    2.15 +
    2.16 +  val BODY = "body"
    2.17 +  val DIV = "div"
    2.18 +  val SPAN = "span"
    2.19 +  val BR = "br"
    2.20 +  val CLASS = "class"
    2.21 +
    2.22 +
    2.23 +  // document markup
    2.24 +
    2.25 +  def body(trees: List[XML.Tree]): XML.Tree =
    2.26 +    XML.Elem(BODY, Nil, trees)
    2.27 +
    2.28 +  def div(trees: List[XML.Tree]): XML.Tree =
    2.29 +    XML.Elem(DIV, Nil, trees)
    2.30 +
    2.31 +  val br: XML.Tree = XML.Elem(BR, Nil, Nil)
    2.32 +
    2.33 +  def spans(tree: XML.Tree): List[XML.Tree] =
    2.34 +    tree match {
    2.35 +      case XML.Elem(name, _, ts) =>
    2.36 +        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
    2.37 +      case text @ XML.Text(txt) =>
    2.38 +        txt.split("\n").toList match {
    2.39 +          case line :: lines if !lines.isEmpty =>
    2.40 +            XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
    2.41 +          case _ => List(text)
    2.42 +        }
    2.43 +    }
    2.44 +}