# HG changeset patch
# User wenzelm
# Date 1363554126 -3600
# Node ID a8e3a72b348c42f51e8d3d9808c65cf88e7ace64
# Parent  8d6e478934dc0df1264340f791d42f36c05605ce
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;

diff -r 8d6e478934dc -r a8e3a72b348c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Mar 17 21:04:38 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Mar 17 22:02:06 2013 +0100
@@ -51,14 +51,14 @@
         case Some(window) => window.descendants()
       }
     val window =
-      if (old_windows.isEmpty) {
-        val window = new Pretty_Tooltip(view, parent, parent_window)
-        window_stack = window :: window_stack
-        window
-      }
-      else {
-        old_windows.foreach(_.dispose)
-        old_windows.last
+      old_windows.reverse match {
+        case Nil =>
+          val window = new Pretty_Tooltip(view, parent, parent_window)
+          window_stack = window :: window_stack
+          window
+        case window :: others =>
+          others.foreach(_.dispose)
+          window
       }
     window.init(rendering, mouse_x, mouse_y, results, body)
     window
@@ -99,6 +99,9 @@
 
   /* main content */
 
+  window.setUndecorated(true)
+  window.getRootPane.setBorder(new LineBorder(Color.BLACK))
+
   private val content_panel =
     new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false }
   window.setContentPane(content_panel)
@@ -143,10 +146,6 @@
     current_results = results
     current_body = body
 
-    window.setUndecorated(true)
-    window.setFocusableWindowState(true)
-    window.getRootPane.setBorder(new LineBorder(Color.BLACK))
-
     pretty_text_area.resize(Rendering.font_family(),
       Rendering.font_size("jedit_tooltip_font_scale").round)
     pretty_text_area.update(rendering.snapshot, results, body)
@@ -172,9 +171,13 @@
         XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
-      window.setSize(new Dimension(100, 100))
-      window.setPreferredSize(new Dimension(100, 100))
+      if (window.getWidth == 0) {
+        window.setSize(new Dimension(100, 100))
+        window.setPreferredSize(new Dimension(100, 100))
+      }
       window.pack
+      window.revalidate
+
       val deco_width = window.getWidth - painter.getWidth
       val deco_height = window.getHeight - painter.getHeight