1.1 --- a/src/Pure/General/symbol.scala	Mon Jun 20 23:25:39 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Jun 21 01:08:15 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 fonts: Map[String, String] =
     1.8 +      Map((
     1.9 +        for ((sym, props) <- symbols if props.isDefinedAt("font"))
    1.10 +          yield (sym -> props("font"))): _*)
    1.11 +
    1.12 +    val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    1.13 +    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
    1.14 +
    1.15      val abbrevs: Map[String, String] =
    1.16        Map((
    1.17          for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))