# HG changeset patch
# User wenzelm
# Date 1281968662 -7200
# Node ID 796904799f4d2e37cfd0a03ce44d9f2df1c92240
# Parent  be39c9e5ac39ef1a2def9529b121720e32881b64
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);

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)
+  }
 }
diff -r be39c9e5ac39 -r 796904799f4d src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Aug 16 12:33:52 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Aug 16 16:24:22 2010 +0200
@@ -159,7 +159,8 @@
         current_body.flatMap(div =>
           Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
             .map(t =>
-              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))), HTML.spans(t))))
+              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
+                HTML.spans(t, true))))
       val doc =
         builder.parse(
           new InputSourceImpl(