CONTROL-mouse management: handle windowDeactivated as well;
some workarounds to robustify html_popup;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 23:47:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 29 17:58:27 2010 +0200
@@ -138,6 +138,7 @@
       case Text.Info(_, Some(msg)) #:: _ =>
         val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
         html_panel.render_sync(List(msg))
+        Thread.sleep(10)  // FIXME !?
         popup.show
         html_popup = Some(popup)
       case _ =>
@@ -169,11 +170,14 @@
   }
 
   private val focus_listener = new FocusAdapter {
-    override def focusLost(e: FocusEvent) { exit_control() }
+    override def focusLost(e: FocusEvent) {
+      highlight_range = None // FIXME exit_control !?
+    }
   }
 
   private val window_listener = new WindowAdapter {
     override def windowIconified(e: WindowEvent) { exit_control() }
+    override def windowDeactivated(e: WindowEvent) { exit_control() }
   }
 
   private val mouse_motion_listener = new MouseMotionAdapter {