author | wenzelm |
Fri, 30 May 2014 10:50:57 +0200 | |
changeset 57126 | 3a928dffc37f |
parent 57116 | 85e55ea7e06d |
child 57127 | a406e15c3cf7 |
--- a/src/Tools/jEdit/src/token_markup.scala Thu May 29 22:46:21 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Fri May 30 10:50:57 2014 +0200 @@ -104,7 +104,7 @@ } private def bold_style(style: SyntaxStyle): SyntaxStyle = - font_style(style, _.deriveFont(Font.BOLD)) + font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD)) val hidden_color: Color = new Color(255, 255, 255, 0)