default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
authorwenzelm
Sun Aug 21 20:04:02 2011 +0200 (2011-08-21)
changeset 443559c38bdc6d755
parent 44354 88bf93c2ae7c
child 44356 f6a2e5ce2ce5
default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 19:32:20 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:04:02 2011 +0200
     1.3 @@ -81,8 +81,10 @@
     1.4  
     1.5    class Style_Extender extends SyntaxUtilities.StyleExtender
     1.6    {
     1.7 -    if (Symbol.font_names.length > 2)
     1.8 -      error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
     1.9 +    val max_user_fonts = 2
    1.10 +    if (Symbol.font_names.length > max_user_fonts)
    1.11 +      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
    1.12 +        Symbol.font_names.mkString(", "))
    1.13  
    1.14      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    1.15      {
    1.16 @@ -93,6 +95,8 @@
    1.17          new_styles(subscript(i.toByte)) = script_style(style, -1)
    1.18          new_styles(superscript(i.toByte)) = script_style(style, 1)
    1.19          new_styles(bold(i.toByte)) = bold_style(style)
    1.20 +        for (idx <- 0 until max_user_fonts)
    1.21 +          new_styles(user_font(idx, i.toByte)) = style
    1.22          for ((family, idx) <- Symbol.font_index)
    1.23            new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
    1.24        }