# HG changeset patch # User wenzelm # Date 1363550678 -3600 # Node ID 8d6e478934dc0df1264340f791d42f36c05605ce # Parent 8d3614b82c80e4bf8d691ece009bc7b86eef2b44 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); diff -r 8d3614b82c80 -r 8d6e478934dc src/Tools/jEdit/src/graphview_dockable.scala --- 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 } } diff -r 8d3614b82c80 -r 8d6e478934dc src/Tools/jEdit/src/pretty_text_area.scala --- 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 _ => } diff -r 8d3614b82c80 -r 8d6e478934dc src/Tools/jEdit/src/pretty_tooltip.scala --- 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() } diff -r 8d3614b82c80 -r 8d6e478934dc src/Tools/jEdit/src/rich_text_area.scala --- 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) } } }