# HG changeset patch
# User wenzelm
# Date 1401447282 -7200
# Node ID 4874411752fe41c9e6cebd109669146f4f6a3040
# Parent  2f620ef839ee9fced439160f0b88237c8a654f57# Parent  a406e15c3cf7122ff93740ede493ff817d2ed71e
merged

diff -r 2f620ef839ee -r 4874411752fe src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 12:27:51 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri May 30 12:54:42 2014 +0200
@@ -351,6 +351,7 @@
                 JEdit_Lib.invalidate_range(text_area, range)
               }
             }
+          dismissed()
           completion_popup = Some(completion)
           view.setKeyEventInterceptor(completion.inner_key_listener)
           JEdit_Lib.invalidate_range(text_area, range)
@@ -576,6 +577,7 @@
                   }
                   override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
                 }
+              dismissed()
               completion_popup = Some(completion)
               completion.show_popup(true)
 
diff -r 2f620ef839ee -r 4874411752fe src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Fri May 30 12:27:51 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Fri May 30 12:54:42 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)