# HG changeset patch
# User wenzelm
# Date 1308767883 -7200
# Node ID d138e7482a1bd7f66b7a3380f649527fbe996a7c
# Parent  17d431c92575e14379f0ce73e64191af7f791828
clarified decoded control symbols;

diff -r 17d431c92575 -r d138e7482a1b src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Jun 22 20:25:35 2011 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jun 22 20:38:03 2011 +0200
@@ -374,10 +374,13 @@
 
     private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
     private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-    val bold_decoded = decode("\\<^bold>")
-
     def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
     def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
-    def is_bold_decoded(sym: String): Boolean = sym == bold_decoded
+
+    val bold_decoded = decode("\\<^bold>")
+    val bsub_decoded = decode("\\<^bsub>")
+    val esub_decoded = decode("\\<^esub>")
+    val bsup_decoded = decode("\\<^bsup>")
+    val esup_decoded = decode("\\<^esup>")
   }
 }
diff -r 17d431c92575 -r d138e7482a1b src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Jun 22 20:25:35 2011 +0200
+++ b/src/Pure/Thy/html.scala	Wed Jun 22 20:38:03 2011 +0200
@@ -82,13 +82,13 @@
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""
             if (s1 == "\n") add(XML.elem(BR))
-            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 (s1 == symbols.bsub_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.esub_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.bsup_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.esup_decoded) t ++= s1  // FIXME
             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 if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
             else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
             else t ++= s1
           }
diff -r 17d431c92575 -r d138e7482a1b src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Jun 22 20:25:35 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Jun 22 20:38:03 2011 +0200
@@ -108,11 +108,11 @@
   def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
     : Map[Text.Offset, Byte => Byte] =
   {
-    // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
+    // FIXME symbols.bsub_decoded etc.
     def ctrl_style(sym: String): Option[Byte => Byte] =
       if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
       else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
-      else if (symbols.is_bold_decoded(sym)) Some(bold(_))
+      else if (sym == symbols.bold_decoded) Some(bold(_))
       else None
 
     var result = Map[Text.Offset, Byte => Byte]()