1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 23:47:45 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 29 17:58:27 2010 +0200
     1.3 @@ -138,6 +138,7 @@
     1.4        case Text.Info(_, Some(msg)) #:: _ =>
     1.5          val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
     1.6          html_panel.render_sync(List(msg))
     1.7 +        Thread.sleep(10)  // FIXME !?
     1.8          popup.show
     1.9          html_popup = Some(popup)
    1.10        case _ =>
    1.11 @@ -169,11 +170,14 @@
    1.12    }
    1.13  
    1.14    private val focus_listener = new FocusAdapter {
    1.15 -    override def focusLost(e: FocusEvent) { exit_control() }
    1.16 +    override def focusLost(e: FocusEvent) {
    1.17 +      highlight_range = None // FIXME exit_control !?
    1.18 +    }
    1.19    }
    1.20  
    1.21    private val window_listener = new WindowAdapter {
    1.22      override def windowIconified(e: WindowEvent) { exit_control() }
    1.23 +    override def windowDeactivated(e: WindowEvent) { exit_control() }
    1.24    }
    1.25  
    1.26    private val mouse_motion_listener = new MouseMotionAdapter {