# HG changeset patch
# User wenzelm
# Date 1260134611 -3600
# Node ID 1fecda9486972b25ef4be5d80c1852b4d5fee060
# Parent  d3b200894e21c9dd61dbe23e166b79baad9eb880
more robust treatment of line breaks -- Java "split" has off semantics;

diff -r d3b200894e21 -r 1fecda948697 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Dec 06 22:22:48 2009 +0100
+++ b/src/Pure/Thy/html.scala	Sun Dec 06 22:23:31 2009 +0100
@@ -6,6 +6,9 @@
 
 package isabelle
 
+import scala.collection.mutable.ListBuffer
+
+
 object HTML
 {
   // common elements and attributes
@@ -14,28 +17,35 @@
   val DIV = "div"
   val SPAN = "span"
   val BR = "br"
+  val PRE = "pre"
   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)
+      case XML.Text(txt) =>
+        val ts = new ListBuffer[XML.Tree]
+        val t = new StringBuilder
+        def flush_text() {
+          if (!t.isEmpty) {
+            ts + XML.Text(t.toString)
+            t.clear
+          }
         }
+        for (sym <- Symbol.elements(txt)) {
+          sym match {
+            case "\n" =>
+              flush_text()
+              ts + XML.elem(BR)
+            case _ =>
+              t ++ sym.toString
+          }
+        }
+        flush_text()
+        ts.toList
     }
 }