avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
authorwenzelm
Sun Aug 21 20:25:49 2011 +0200 (2011-08-21)
changeset 44356f6a2e5ce2ce5
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
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:04:02 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:25:49 2011 +0200
     1.3 @@ -79,6 +79,8 @@
     1.4    private def bold_style(style: SyntaxStyle): SyntaxStyle =
     1.5      font_style(style, _.deriveFont(Font.BOLD))
     1.6  
     1.7 +  private def hidden_color: Color = new Color(255, 255, 255, 0)
     1.8 +
     1.9    class Style_Extender extends SyntaxUtilities.StyleExtender
    1.10    {
    1.11      val max_user_fonts = 2
    1.12 @@ -101,7 +103,7 @@
    1.13            new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
    1.14        }
    1.15        new_styles(hidden) =
    1.16 -        new SyntaxStyle(Color.white, null,
    1.17 +        new SyntaxStyle(hidden_color, null,
    1.18            { val font = styles(0).getFont
    1.19              transform_font(new Font(font.getFamily, 0, 1),
    1.20                AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })