# HG changeset patch # User wenzelm # Date 1379788263 -7200 # Node ID 29eaacff407840f396a0bdfd357d5b122022b8d9 # Parent 06a6216f733ed338b8646695f14bb4c7b9bce6fd proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows); diff -r 06a6216f733e -r 29eaacff4078 src/Pure/System/gui.scala --- a/src/Pure/System/gui.scala Sat Sep 21 19:48:46 2013 +0200 +++ b/src/Pure/System/gui.scala Sat Sep 21 20:31:03 2013 +0200 @@ -8,7 +8,7 @@ import java.awt.{Image, Component, Container, Toolkit, Window} -import javax.swing.{ImageIcon, JOptionPane, UIManager} +import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow} import scala.swing.{ComboBox, TextArea, ScrollPane} import scala.swing.event.SelectionChanged @@ -143,5 +143,12 @@ def parent_window(component: Component): Option[Window] = ancestors(component).collectFirst({ case x: Window => x }) + + def layered_pane(component: Component): Option[JLayeredPane] = + parent_window(component) match { + case Some(window: JWindow) => Some(window.getLayeredPane) + case Some(frame: JFrame) => Some(frame.getLayeredPane) + case _ => None + } } diff -r 06a6216f733e -r 29eaacff4078 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Sep 21 19:48:46 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Sep 21 20:31:03 2013 +0200 @@ -11,7 +11,7 @@ import java.awt.{Color, Point, BorderLayout, Dimension} import java.awt.event.{FocusAdapter, FocusEvent} -import javax.swing.{JPanel, JComponent, SwingUtilities} +import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane} import javax.swing.border.LineBorder import scala.swing.{FlowPanel, Label} @@ -42,25 +42,28 @@ location: Point, rendering: Rendering, results: Command.Results, - info: Text.Info[XML.Body]): Pretty_Tooltip = + info: Text.Info[XML.Body]) { Swing_Thread.require() stack match { case top :: _ if top.results == results && top.info == info => top case _ => - val (old, rest) = - GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { - case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) - case None => (stack, Nil) - } - old.foreach(_.hide_popup) + GUI.layered_pane(parent) match { + case None => + case Some(layered) => + val (old, rest) = + GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { + case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) + case None => (stack, Nil) + } + old.foreach(_.hide_popup) - val loc = SwingUtilities.convertPoint(parent, location, view.getLayeredPane) - val tip = new Pretty_Tooltip(view, loc, rendering, results, info) - stack = tip :: rest - tip.show_popup - tip + val loc = SwingUtilities.convertPoint(parent, location, layered) + val tip = new Pretty_Tooltip(view, layered, loc, rendering, results, info) + stack = tip :: rest + tip.show_popup + } } } @@ -139,6 +142,7 @@ class Pretty_Tooltip private( view: View, + layered: JLayeredPane, location: Point, rendering: Rendering, private val results: Command.Results, @@ -218,7 +222,6 @@ private val popup = { - val layered = view.getLayeredPane val screen = JEdit_Lib.screen_location(layered, location) val size = {