# HG changeset patch
# User wenzelm
# Date 1313949842 -7200
# Node ID 9c38bdc6d755e94701f99668e6fbb3adba774313
# Parent  88bf93c2ae7c1dd06f23eb1b77bf38295b6d8d9f
default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;

diff -r 88bf93c2ae7c -r 9c38bdc6d755 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 19:32:20 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:04:02 2011 +0200
@@ -81,8 +81,10 @@
 
   class Style_Extender extends SyntaxUtilities.StyleExtender
   {
-    if (Symbol.font_names.length > 2)
-      error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
+    val max_user_fonts = 2
+    if (Symbol.font_names.length > max_user_fonts)
+      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
+        Symbol.font_names.mkString(", "))
 
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
     {
@@ -93,6 +95,8 @@
         new_styles(subscript(i.toByte)) = script_style(style, -1)
         new_styles(superscript(i.toByte)) = script_style(style, 1)
         new_styles(bold(i.toByte)) = bold_style(style)
+        for (idx <- 0 until max_user_fonts)
+          new_styles(user_font(idx, i.toByte)) = style
         for ((family, idx) <- Symbol.font_index)
           new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
       }