src/Pure/Thy/html.scala
changeset 34006 bbd146caa6b2
parent 34004 30c8746074d0
child 34046 8e743ca417b9
     1.1 --- a/src/Pure/Thy/html.scala	Mon Dec 07 00:02:07 2009 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Mon Dec 07 00:02:54 2009 +0100
     1.3 @@ -51,17 +51,17 @@
     1.4          val syms = Symbol.elements(txt)
     1.5          while (syms.hasNext) {
     1.6            val s1 = syms.next
     1.7 -          lazy val s2 = if (syms.hasNext) syms.next else ""
     1.8 +          def s2() = if (syms.hasNext) syms.next else ""
     1.9            s1 match {
    1.10              case "\n" => add(XML.elem(BR))
    1.11              case "\\<^bsub>" => t ++ s1  // FIXME
    1.12              case "\\<^esub>" => t ++ s1  // FIXME
    1.13              case "\\<^bsup>" => t ++ s1  // FIXME
    1.14              case "\\<^esup>" => t ++ s1  // FIXME
    1.15 -            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2))
    1.16 -            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2))
    1.17 -            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2))))
    1.18 -            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2))))
    1.19 +            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    1.20 +            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    1.21 +            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.22 +            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    1.23              case _ => t ++ s1
    1.24            }
    1.25          }