explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 16 21:44:04 2013 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Mar 17 21:04:38 2013 +0100
@@ -65,7 +65,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             val rendering = Rendering(snapshot, PIDE.options.value)
-            new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
+            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
             null
           }
         }

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 16 21:44:04 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 17 21:04:38 2013 +0100
@@ -54,7 +54,6 @@
 
 class Pretty_Text_Area(
   view: View,
-  background: Option[Color] = None,
   close_action: () => Unit = () => (),
   propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
 {
@@ -95,7 +94,6 @@
 
     getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
     getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
-    background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
     getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
     getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
     getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
@@ -169,10 +167,7 @@
           Registers.copy(text_area, '$')
           evt.consume
         case KeyEvent.VK_ESCAPE =>
-          Window.getWindows foreach {
-            case c: Pretty_Tooltip => c.dispose
-            case _ =>
-          }
+          Pretty_Tooltip.windows().foreach(_.dispose)
           evt.consume
         case _ =>
       }

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 16 21:44:04 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Mar 17 21:04:38 2013 +0100
@@ -21,46 +21,89 @@
 import org.gjt.sp.jedit.textarea.TextArea
 
 
-class Pretty_Tooltip(
-  view: View,
-  parent: JComponent,
-  rendering: Rendering,
-  mouse_x: Int, mouse_y: Int,
-  results: Command.Results,
-  body: XML.Body)
-  extends JDialog(JEdit_Lib.parent_window(parent) getOrElse view)
+object Pretty_Tooltip
+{
+  /* window stack -- owned by Swing thread */
+
+  private var window_stack: List[Pretty_Tooltip] = Nil
+
+  def windows(): List[Pretty_Tooltip] =
+  {
+    Swing_Thread.require()
+    window_stack
+  }
+
+  def apply(
+    view: View,
+    parent: JComponent,
+    rendering: Rendering,
+    mouse_x: Int, mouse_y: Int,
+    results: Command.Results,
+    body: XML.Body): Pretty_Tooltip =
+  {
+    Swing_Thread.require()
+
+    val parent_window = JEdit_Lib.parent_window(parent) getOrElse view
+
+    val old_windows =
+      windows().find(_ == parent_window) match {
+        case None => windows()
+        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
+      }
+    window.init(rendering, mouse_x, mouse_y, results, body)
+    window
+  }
+}
+
+
+class Pretty_Tooltip private(view: View, parent: JComponent, parent_window: Window)
+  extends JDialog(parent_window)
 {
   window =>
 
   Swing_Thread.require()
 
 
-  window.setUndecorated(true)
-  window.setFocusableWindowState(true)
+  /* implicit state -- owned by Swing thread */
+
+  private var current_rendering: Rendering =
+    Rendering(Document.State.init.snapshot(), PIDE.options.value)
+  private var current_results = Command.Results.empty
+  private var current_body: XML.Body = Nil
+
+
+  /* window hierarchy */
+
+  def descendants(): List[Pretty_Tooltip] =
+    if (Pretty_Tooltip.windows().exists(_ == window))
+      Pretty_Tooltip.windows().takeWhile(_ != window)
+    else Nil
 
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) {
-      if (!Window.getWindows.exists(w =>
-            w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
+      if (!descendants().exists(_.isDisplayable))
         window.dispose()
     }
   })
 
-  window.setContentPane(new JPanel(new BorderLayout) {
-    setBackground(rendering.tooltip_color)
-    override def getFocusTraversalKeysEnabled(): Boolean = false
-  })
-  window.getRootPane.setBorder(new LineBorder(Color.BLACK))
 
+  /* main content */
 
-  /* pretty text area */
+  private val content_panel =
+    new JPanel(new BorderLayout) { override def getFocusTraversalKeysEnabled = false }
+  window.setContentPane(content_panel)
 
-  val pretty_text_area =
-    new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true)
-  pretty_text_area.resize(Rendering.font_family(),
-    Rendering.font_size("jedit_tooltip_font_scale").round)
-  pretty_text_area.update(rendering.snapshot, results, body)
-
+  val pretty_text_area = new Pretty_Text_Area(view, () => window.dispose(), true)
   window.add(pretty_text_area)
 
 
@@ -79,57 +122,83 @@
     listenTo(mouse.clicks)
     reactions += {
       case _: MouseClicked =>
-        Info_Dockable(view, rendering.snapshot, results, body)
+        Info_Dockable(view, current_rendering.snapshot, current_results, current_body)
         window.dispose()
     }
   }
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
-    background = rendering.tooltip_color
-  }
+  private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach)
   window.add(controls.peer, BorderLayout.NORTH)
 
 
-  /* window geometry */
+  /* refresh */
 
-  val screen_point = new Point(mouse_x, mouse_y)
-  SwingUtilities.convertPointToScreen(screen_point, parent)
-  val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
-
+  def init(
+    rendering: Rendering,
+    mouse_x: Int, mouse_y: Int,
+    results: Command.Results,
+    body: XML.Body)
   {
-    val painter = pretty_text_area.getPainter
-    val fm = painter.getFontMetrics
-    val margin = rendering.tooltip_margin
-    val lines =
-      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
-        (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+    current_rendering = rendering
+    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)
 
-    window.setSize(new Dimension(100, 100))
-    window.setPreferredSize(new Dimension(100, 100))
-    window.pack
-    val deco_width = window.getWidth - painter.getWidth
-    val deco_height = window.getHeight - painter.getHeight
+    val background = rendering.tooltip_color
+    content_panel.setBackground(background)
+    controls.background = background
+    pretty_text_area.getPainter.setBackground(background)
+    pretty_text_area.getGutter.setBackground(background)
+
+
+    /* window geometry */
+
+    val screen_point = new Point(mouse_x, mouse_y)
+    SwingUtilities.convertPointToScreen(screen_point, parent)
+    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
 
-    val bounds = rendering.tooltip_bounds
-    val w =
-      ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
-      (screen_bounds.width * bounds).toInt
-    val h =
-      (fm.getHeight * (lines + 1) + deco_height) min
-      (screen_bounds.height * bounds).toInt
+    {
+      val painter = pretty_text_area.getPainter
+      val fm = painter.getFontMetrics
+      val margin = rendering.tooltip_margin
+      val lines =
+        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))
+      window.pack
+      val deco_width = window.getWidth - painter.getWidth
+      val deco_height = window.getHeight - painter.getHeight
 
-    window.setSize(new Dimension(w, h))
-    window.setPreferredSize(new Dimension(w, h))
-    window.pack
-    window.revalidate
+      val bounds = rendering.tooltip_bounds
+      val w =
+        ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+        (screen_bounds.width * bounds).toInt
+      val h =
+        (fm.getHeight * (lines + 1) + deco_height) min
+        (screen_bounds.height * bounds).toInt
 
-    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
-    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
-    window.setLocation(x, y)
+      window.setSize(new Dimension(w, h))
+      window.setPreferredSize(new Dimension(w, h))
+      window.pack
+      window.revalidate
+
+      val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
+      val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
+      window.setLocation(x, y)
+    }
+
+    window.setVisible(true)
+    pretty_text_area.requestFocus
+    pretty_text_area.refresh()
   }
-
-  window.setVisible(true)
-  pretty_text_area.requestFocus
-  pretty_text_area.refresh()
 }
 

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 16 21:44:04 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Mar 17 21:04:38 2013 +0100
@@ -220,7 +220,7 @@
                   val painter = text_area.getPainter
                   val y1 = y + painter.getFontMetrics.getHeight / 2
                   val results = rendering.command_results(range)
-                  new Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+                  Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
                 }
             }
           }