prefer JDialog over JWindow to avoid focus inversion problem on Compiz (e.g. Ubuntu/Unity 12.10): both JDialog and JFrame happen to work, but JFrame does not support parent nesting;
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Dec 31 21:01:00 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Dec 31 21:41:22 2012 +0100
@@ -11,7 +11,7 @@
import java.awt.{Color, Point, BorderLayout, Window, Dimension}
import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
-import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
+import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent, KeyStroke}
import javax.swing.border.LineBorder
import scala.swing.{FlowPanel, Label}
@@ -28,13 +28,17 @@
mouse_x: Int, mouse_y: Int,
results: Command.Results,
body: XML.Body)
- extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
+ extends JDialog(JEdit_Lib.parent_window(parent) getOrElse view)
{
window =>
Swing_Thread.require()
+ window.setUndecorated(true)
+ window.setFocusableWindowState(true)
+ window.setAutoRequestFocus(true)
+
window.addWindowFocusListener(new WindowAdapter {
override def windowLostFocus(e: WindowEvent) {
if (!Window.getWindows.exists(w =>