# HG changeset patch
# User wenzelm
# Date 1308490276 -7200
# Node ID def9784a33160ead3848042ce62bf5c5cd0fbb5d
# Parent  b55a273ede187d36af7310620cce3e20d620a356
tuned;

diff -r b55a273ede18 -r def9784a3316 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
+++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:31:16 2011 +0200
@@ -49,6 +49,7 @@
 
   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 bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
 
   def spans(symbols: Symbol.Interpretation,
     input: XML.Tree, original_data: Boolean = false): XML.Body =
@@ -77,15 +78,13 @@
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""
             if (s1 == "\n") add(XML.elem(BR))
-            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
-            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
             else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
             else if (s1 == "\\<^esub>") t ++= s1  // FIXME
             else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
             else if (s1 == "\\<^esup>") t ++= s1  // FIXME
-            else if (symbols.is_bold_decoded(s1)) {
-              add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
-            }
+            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
+            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
+            else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
             else t ++= s1
           }
           flush()