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>"))