# HG changeset patch
# User wenzelm
# Date 1260140574 -3600
# Node ID bbd146caa6b2545c05498e3975c7d87d36d7b171
# Parent  ada5098506aff529b0fd8c85d724a6ce03513f12
avoid lazy val with side-effects -- spurious null pointers!?

diff -r ada5098506af -r bbd146caa6b2 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Dec 07 00:02:07 2009 +0100
+++ b/src/Pure/Thy/html.scala	Mon Dec 07 00:02:54 2009 +0100
@@ -51,17 +51,17 @@
         val syms = Symbol.elements(txt)
         while (syms.hasNext) {
           val s1 = syms.next
-          lazy val s2 = if (syms.hasNext) syms.next else ""
+          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 "\\<^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
           }
         }