# 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]()