# HG changeset patch
# User wenzelm
# Date 1401439857 -7200
# Node ID 3a928dffc37f33644042345ac4cdb0725a1bbfb2
# Parent  85e55ea7e06da111b1b298b5d1ea6d3b5b9c6a91
more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;

diff -r 85e55ea7e06d -r 3a928dffc37f 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)