1.1 --- a/src/Pure/Thy/html.scala	Mon Aug 16 12:33:52 2010 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Mon Aug 16 16:24:22 2010 +0200
     1.3 @@ -50,41 +50,47 @@
     1.4    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
     1.5    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
     1.6  
     1.7 -  def spans(tree: XML.Tree): List[XML.Tree] =
     1.8 -    tree match {
     1.9 -      case XML.Elem(Markup(name, _), ts) =>
    1.10 -        List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans)))))
    1.11 -      case XML.Text(txt) =>
    1.12 -        val ts = new ListBuffer[XML.Tree]
    1.13 -        val t = new StringBuilder
    1.14 -        def flush() {
    1.15 -          if (!t.isEmpty) {
    1.16 -            ts += XML.Text(t.toString)
    1.17 -            t.clear
    1.18 +  def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
    1.19 +  {
    1.20 +    def html_spans(tree: XML.Tree): List[XML.Tree] =
    1.21 +      tree match {
    1.22 +        case XML.Elem(Markup(name, _), ts) =>
    1.23 +          if (original_data)
    1.24 +            List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
    1.25 +          else List(span(name, ts.flatMap(html_spans)))
    1.26 +        case XML.Text(txt) =>
    1.27 +          val ts = new ListBuffer[XML.Tree]
    1.28 +          val t = new StringBuilder
    1.29 +          def flush() {
    1.30 +            if (!t.isEmpty) {
    1.31 +              ts += XML.Text(t.toString)
    1.32 +              t.clear
    1.33 +            }
    1.34            }
    1.35 -        }
    1.36 -        def add(elem: XML.Tree) {
    1.37 +          def add(elem: XML.Tree) {
    1.38 +            flush()
    1.39 +            ts += elem
    1.40 +          }
    1.41 +          val syms = Symbol.iterator(txt).map(_.toString)
    1.42 +          while (syms.hasNext) {
    1.43 +            val s1 = syms.next
    1.44 +            def s2() = if (syms.hasNext) syms.next else ""
    1.45 +            s1 match {
    1.46 +              case "\n" => add(XML.elem(BR))
    1.47 +              case "\\<^bsub>" => t ++= s1  // FIXME
    1.48 +              case "\\<^esub>" => t ++= s1  // FIXME
    1.49 +              case "\\<^bsup>" => t ++= s1  // FIXME
    1.50 +              case "\\<^esup>" => t ++= s1  // FIXME
    1.51 +              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    1.52 +              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    1.53 +              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.54 +              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    1.55 +              case _ => t ++= s1
    1.56 +            }
    1.57 +          }
    1.58            flush()
    1.59 -          ts += elem
    1.60 -        }
    1.61 -        val syms = Symbol.iterator(txt).map(_.toString)
    1.62 -        while (syms.hasNext) {
    1.63 -          val s1 = syms.next
    1.64 -          def s2() = if (syms.hasNext) syms.next else ""
    1.65 -          s1 match {
    1.66 -            case "\n" => add(XML.elem(BR))
    1.67 -            case "\\<^bsub>" => t ++= s1  // FIXME
    1.68 -            case "\\<^esub>" => t ++= s1  // FIXME
    1.69 -            case "\\<^bsup>" => t ++= s1  // FIXME
    1.70 -            case "\\<^esup>" => t ++= s1  // FIXME
    1.71 -            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    1.72 -            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    1.73 -            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.74 -            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    1.75 -            case _ => t ++= s1
    1.76 -          }
    1.77 -        }
    1.78 -        flush()
    1.79 -        ts.toList
    1.80 -    }
    1.81 +          ts.toList
    1.82 +      }
    1.83 +    html_spans(input)
    1.84 +  }
    1.85  }