avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
authorwenzelm
Sun, 21 Aug 2011 20:25:49 +0200
changeset 44356 f6a2e5ce2ce5
parent 44355 9c38bdc6d755
child 44357 5f5649ac8235
avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:04:02 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:25:49 2011 +0200
@@ -79,6 +79,8 @@
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
     font_style(style, _.deriveFont(Font.BOLD))
 
+  private def hidden_color: Color = new Color(255, 255, 255, 0)
+
   class Style_Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2
@@ -101,7 +103,7 @@
           new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
       }
       new_styles(hidden) =
-        new SyntaxStyle(Color.white, null,
+        new SyntaxStyle(hidden_color, null,
           { val font = styles(0).getFont
             transform_font(new Font(font.getFamily, 0, 1),
               AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })