1.1 --- a/src/Pure/General/symbol.scala	Tue Jun 21 01:08:15 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Jun 21 12:53:55 2011 +0200
     1.3 @@ -234,6 +234,14 @@
     1.4        Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     1.5      }
     1.6  
     1.7 +    val abbrevs: Map[String, String] =
     1.8 +      Map((
     1.9 +        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
    1.10 +          yield (sym -> props("abbrev"))): _*)
    1.11 +
    1.12 +
    1.13 +    /* user fonts */
    1.14 +
    1.15      val fonts: Map[String, String] =
    1.16        Map((
    1.17          for ((sym, props) <- symbols if props.isDefinedAt("font"))
    1.18 @@ -242,10 +250,7 @@
    1.19      val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    1.20      val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
    1.21  
    1.22 -    val abbrevs: Map[String, String] =
    1.23 -      Map((
    1.24 -        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
    1.25 -          yield (sym -> props("abbrev"))): _*)
    1.26 +    def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
    1.27  
    1.28  
    1.29      /* main recoder methods */
    1.30 @@ -336,10 +341,16 @@
    1.31        sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
    1.32  
    1.33  
    1.34 -    /* special control symbols */
    1.35 +    /* control symbols */
    1.36 +
    1.37 +    private val ctrl_decoded: Set[String] =
    1.38 +      Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
    1.39 +
    1.40 +    def is_ctrl(sym: String): Boolean =
    1.41 +      sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
    1.42  
    1.43      def is_controllable(sym: String): Boolean =
    1.44 -      !is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
    1.45 +      !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
    1.46  
    1.47      private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    1.48      private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))

     2.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 01:08:15 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 12:53:55 2011 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4    /* extended syntax styles */
     2.5  
     2.6    private val plain_range: Int = JEditToken.ID_COUNT
     2.7 +  private val full_range = 6 * plain_range + 1
     2.8    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
     2.9  
    2.10    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    2.11 @@ -50,7 +51,6 @@
    2.12    {
    2.13      if (symbols.font_names.length > 2)
    2.14        error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
    2.15 -    private val full_range: Int = (4 + symbols.font_names.length) * plain_range + 1
    2.16  
    2.17      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    2.18      {
    2.19 @@ -99,10 +99,8 @@
    2.20          }
    2.21          ctrl = ""
    2.22        }
    2.23 -      // FIXME avoid symbols.encode!?
    2.24 -      symbols.fonts.get(symbols.encode(sym)) match {
    2.25 -        case Some(font) =>
    2.26 -          mark(offset, offset + sym.length, user_font(symbols.font_index(font), _))
    2.27 +      symbols.lookup_font(sym) match {
    2.28 +        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
    2.29          case _ =>
    2.30        }
    2.31        offset += sym.length