# HG changeset patch
# User wenzelm
# Date 1372536910 -7200
# Node ID 23a09c6397003d42392ba2fd8bdb5d727c24183b
# Parent  478ef4fa3d5a65b0d76497304ca5d72aa1b7abcb
avoid potential race condition of focusLost/dismiss vs. popup.show;

diff -r 478ef4fa3d5a -r 23a09c639700 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 21:28:24 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 22:15:10 2013 +0200
@@ -55,6 +55,7 @@
 
     val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, body)
     stack = tip :: rest
+    tip.show_popup
     tip
   }
 
@@ -221,9 +222,12 @@
     PopupFactory.getSharedInstance.getPopup(parent, tip, x, y)
   }
 
-  popup.show
-  pretty_text_area.requestFocus
-  pretty_text_area.update(rendering.snapshot, results, body)
+  private def show_popup
+  {
+    popup.show
+    pretty_text_area.requestFocus
+    pretty_text_area.update(rendering.snapshot, results, body)
+  }
 
   private def hide_popup: Unit = popup.hide
 }