--- a/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 20:34:46 2013 +0200
@@ -28,8 +28,7 @@
/* editing support for control symbols */
val is_control_style =
- Set(Symbol.sub_decoded, Symbol.sup_decoded,
- Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
+ Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.bold_decoded)
def update_control_style(control: String, text: String): String =
{
@@ -161,8 +160,8 @@
{
// FIXME Symbol.bsub_decoded etc.
def control_style(sym: String): Option[Byte => Byte] =
- if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
- else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
+ if (sym == Symbol.sub_decoded) Some(subscript(_))
+ else if (sym == Symbol.sup_decoded) Some(superscript(_))
else if (sym == Symbol.bold_decoded) Some(bold(_))
else None