1.1 --- a/src/Pure/General/symbol.scala	Sun Jun 19 00:03:44 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sun Jun 19 14:11:06 2011 +0200
     1.3 @@ -326,7 +326,19 @@
     1.4      def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
     1.5      def is_symbolic(sym: String): Boolean =
     1.6        sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
     1.7 +
     1.8 +
     1.9 +    /* special control symbols */
    1.10 +
    1.11      def is_controllable(sym: String): Boolean =
    1.12        !is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
    1.13 +
    1.14 +    private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    1.15 +    private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
    1.16 +    val bold_decoded = decode("\\<^bold>")
    1.17 +
    1.18 +    def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
    1.19 +    def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
    1.20 +    def is_bold_decoded(sym: String): Boolean = sym == bold_decoded
    1.21    }
    1.22  }