1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jul 07 13:48:30 2011 +0200
     1.3 @@ -81,9 +81,8 @@
     1.4  
     1.5    class Style_Extender extends SyntaxUtilities.StyleExtender
     1.6    {
     1.7 -    val symbols = Isabelle_System.symbols
     1.8 -    if (symbols.font_names.length > 2)
     1.9 -      error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
    1.10 +    if (Symbol.font_names.length > 2)
    1.11 +      error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
    1.12  
    1.13      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    1.14      {
    1.15 @@ -94,7 +93,7 @@
    1.16          new_styles(subscript(i.toByte)) = script_style(style, -1)
    1.17          new_styles(superscript(i.toByte)) = script_style(style, 1)
    1.18          new_styles(bold(i.toByte)) = bold_style(style)
    1.19 -        for ((family, idx) <- symbols.font_index)
    1.20 +        for ((family, idx) <- Symbol.font_index)
    1.21            new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
    1.22        }
    1.23        new_styles(hidden) =
    1.24 @@ -108,13 +107,11 @@
    1.25  
    1.26    def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
    1.27    {
    1.28 -    val symbols = Isabelle_System.symbols
    1.29 -
    1.30 -    // FIXME symbols.bsub_decoded etc.
    1.31 +    // FIXME Symbol.is_bsub_decoded etc.
    1.32      def ctrl_style(sym: String): Option[Byte => Byte] =
    1.33 -      if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
    1.34 -      else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
    1.35 -      else if (sym == symbols.bold_decoded) Some(bold(_))
    1.36 +      if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
    1.37 +      else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
    1.38 +      else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
    1.39        else None
    1.40  
    1.41      var result = Map[Text.Offset, Byte => Byte]()
    1.42 @@ -127,13 +124,13 @@
    1.43      for (sym <- Symbol.iterator(text)) {
    1.44        if (ctrl_style(sym).isDefined) ctrl = sym
    1.45        else if (ctrl != "") {
    1.46 -        if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
    1.47 +        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
    1.48            mark(offset - ctrl.length, offset, _ => hidden)
    1.49            mark(offset, offset + sym.length, ctrl_style(ctrl).get)
    1.50          }
    1.51          ctrl = ""
    1.52        }
    1.53 -      symbols.lookup_font(sym) match {
    1.54 +      Symbol.lookup_font(sym) match {
    1.55          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
    1.56          case _ =>
    1.57        }