diff -r be39c9e5ac39 -r 796904799f4d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Aug 16 12:33:52 2010 +0200
+++ b/src/Pure/Thy/html.scala	Mon Aug 16 16:24:22 2010 +0200
@@ -50,41 +50,47 @@
   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
 
-  def spans(tree: XML.Tree): List[XML.Tree] =
-    tree match {
-      case XML.Elem(Markup(name, _), ts) =>
-        List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans)))))
-      case XML.Text(txt) =>
-        val ts = new ListBuffer[XML.Tree]
-        val t = new StringBuilder
-        def flush() {
-          if (!t.isEmpty) {
-            ts += XML.Text(t.toString)
-            t.clear
+  def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
+  {
+    def html_spans(tree: XML.Tree): List[XML.Tree] =
+      tree match {
+        case XML.Elem(Markup(name, _), ts) =>
+          if (original_data)
+            List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
+          else List(span(name, ts.flatMap(html_spans)))
+        case XML.Text(txt) =>
+          val ts = new ListBuffer[XML.Tree]
+          val t = new StringBuilder
+          def flush() {
+            if (!t.isEmpty) {
+              ts += XML.Text(t.toString)
+              t.clear
+            }
           }
-        }
-        def add(elem: XML.Tree) {
+          def add(elem: XML.Tree) {
+            flush()
+            ts += elem
+          }
+          val syms = Symbol.iterator(txt).map(_.toString)
+          while (syms.hasNext) {
+            val s1 = syms.next
+            def s2() = if (syms.hasNext) syms.next else ""
+            s1 match {
+              case "\n" => add(XML.elem(BR))
+              case "\\<^bsub>" => t ++= s1  // FIXME
+              case "\\<^esub>" => t ++= s1  // FIXME
+              case "\\<^bsup>" => t ++= s1  // FIXME
+              case "\\<^esup>" => t ++= s1  // FIXME
+              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
+              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
+              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
+              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
+              case _ => t ++= s1
+            }
+          }
           flush()
-          ts += elem
-        }
-        val syms = Symbol.iterator(txt).map(_.toString)
-        while (syms.hasNext) {
-          val s1 = syms.next
-          def s2() = if (syms.hasNext) syms.next else ""
-          s1 match {
-            case "\n" => add(XML.elem(BR))
-            case "\\<^bsub>" => t ++= s1  // FIXME
-            case "\\<^esub>" => t ++= s1  // FIXME
-            case "\\<^bsup>" => t ++= s1  // FIXME
-            case "\\<^esup>" => t ++= s1  // FIXME
-            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
-            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
-            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
-            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
-            case _ => t ++= s1
-          }
-        }
-        flush()
-        ts.toList
-    }
+          ts.toList
+      }
+    html_spans(input)
+  }
 }