more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
authorwenzelm
Fri, 30 May 2014 10:50:57 +0200
changeset 57126 3a928dffc37f
parent 57116 85e55ea7e06d
child 57127 a406e15c3cf7
more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
src/Tools/jEdit/src/token_markup.scala
--- 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)