# HG changeset patch
# User wenzelm
# Date 1285775907 -7200
# Node ID b59e064e32c3013b31457e8919a00c6f3b428f8c
# Parent  62b91eb2d39aea89837b43dcf09f7acd7b74d505
CONTROL-mouse management: handle windowDeactivated as well;
some workarounds to robustify html_popup;

diff -r 62b91eb2d39a -r b59e064e32c3 src/Tools/jEdit/src/jedit/document_view.scala
--- 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 {