avoid potential race condition of focusLost/dismiss vs. popup.show;

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