merged

--- 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)
 

--- 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)