Basic HTML output.

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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/html.scala	Fri Dec 04 22:51:59 2009 +0100
@@ -0,0 +1,41 @@
+/*  Title:      Pure/Thy/html.scala
+    Author:     Makarius
+
+Basic HTML output.
+*/
+
+package isabelle
+
+object HTML
+{
+  // common elements and attributes
+
+  val BODY = "body"
+  val DIV = "div"
+  val SPAN = "span"
+  val BR = "br"
+  val CLASS = "class"
+
+
+  // document markup
+
+  def body(trees: List[XML.Tree]): XML.Tree =
+    XML.Elem(BODY, Nil, trees)
+
+  def div(trees: List[XML.Tree]): XML.Tree =
+    XML.Elem(DIV, Nil, trees)
+
+  val br: XML.Tree = XML.Elem(BR, Nil, Nil)
+
+  def spans(tree: XML.Tree): List[XML.Tree] =
+    tree match {
+      case XML.Elem(name, _, ts) =>
+        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
+      case text @ XML.Text(txt) =>
+        txt.split("\n").toList match {
+          case line :: lines if !lines.isEmpty =>
+            XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
+          case _ => List(text)
+        }
+    }
+}