uniform use of isabelle.jEdit.Popup, based on generic screen location operations;

--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -249,41 +249,16 @@
 
   private val popup =
   {
-    val screen_point = new Point(location.x, location.y)
-    SwingUtilities.convertPointToScreen(screen_point, layered)
-    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
-
-    val w0 = layered.getWidth
-    val h0 = layered.getHeight
-
-    val (w, h) =
+    val screen = JEdit_Lib.screen_location(layered, location)
+    val size =
     {
       val geometry = JEdit_Lib.window_geometry(completion, completion)
       val bounds = Rendering.popup_bounds
-      val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
-      val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
-      (w, h)
+      val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
+      val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
+      new Dimension(w, h)
     }
-
-    val (x, y) =
-    {
-      val x0 = layered.getLocationOnScreen.x
-      val y0 = layered.getLocationOnScreen.y
-      val x1 = x0 + w0 - w
-      val y1 = y0 + h0 - h
-      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
-      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
-
-      val point = new Point((x2 min x1) max x0, (y2 min y1) max y0)
-      SwingUtilities.convertPointFromScreen(point, layered)
-      (point.x, point.y)
-    }
-
-    completion.setLocation(x, y)
-    completion.setSize(new Dimension(w, h))
-    completion.setPreferredSize(new Dimension(w, h))
-
-    new Popup(layered, completion)
+    new Popup(layered, completion, screen.relative(layered, size), size)
   }
 
   private def show_popup()

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import javax.swing.{SwingUtilities, JComponent}
+import javax.swing.JComponent
 import java.awt.Point
 import java.awt.event.{WindowFocusListener, WindowEvent}
 
@@ -66,10 +66,8 @@
             Pretty_Tooltip.invoke(() =>
               {
                 val rendering = Rendering(snapshot, PIDE.options.value)
-                val screen_point = new Point(x, y)
-                SwingUtilities.convertPointToScreen(screen_point, parent)
                 val info = Text.Info(Text.Range(~1), body)
-                Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, info)
+                Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
               })
             null
           }

--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -9,9 +9,9 @@
 
 import isabelle._
 
-import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
+import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
 import java.awt.event.{KeyEvent, KeyListener}
-import javax.swing.{Icon, ImageIcon, JWindow}
+import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
 import scala.annotation.tailrec
 
@@ -23,16 +23,42 @@
 
 object JEdit_Lib
 {
-  /* bounds within multi-screen environment */
+  /* location within multi-screen environment */
+
+  final case class Screen_Location(point: Point, bounds: Rectangle)
+  {
+    def relative(parent: Component, size: Dimension): Point =
+    {
+      val w = size.width
+      val h = size.height
 
-  def screen_bounds(screen_point: Point): Rectangle =
+      val x0 = parent.getLocationOnScreen.x
+      val y0 = parent.getLocationOnScreen.y
+      val x1 = x0 + parent.getWidth - w
+      val y1 = y0 + parent.getHeight - h
+      val x2 = point.x min (bounds.x + bounds.width - w)
+      val y2 = point.y min (bounds.y + bounds.height - h)
+
+      val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
+      SwingUtilities.convertPointFromScreen(location, parent)
+      location
+    }
+  }
+
+  def screen_location(component: Component, point: Point): Screen_Location =
   {
+    val screen_point = new Point(point.x, point.y)
+    SwingUtilities.convertPointToScreen(screen_point, component)
+
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
-    (for {
-      device <- ge.getScreenDevices.iterator
-      config <- device.getConfigurations.iterator
-      bounds = config.getBounds
-    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
+    val screen_bounds =
+      (for {
+        device <- ge.getScreenDevices.iterator
+        config <- device.getConfigurations.iterator
+        bounds = config.getBounds
+      } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
+
+    Screen_Location(screen_point, screen_bounds)
   }
 
 

--- a/src/Tools/jEdit/src/popup.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/popup.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/popup.scala
     Author:     Makarius
 
-Simple popup within layered pane, based on component with given geometry.
+Popup within layered pane.
 */
 
 package isabelle.jedit
@@ -9,17 +9,24 @@
 
 import isabelle._
 
+import java.awt.{Point, Dimension}
 import javax.swing.{JLayeredPane, JComponent}
 
 
 class Popup(
   layered: JLayeredPane,
-  component: JComponent) extends javax.swing.Popup()
+  component: JComponent,
+  location: Point,
+  size: Dimension) extends javax.swing.Popup()
 {
   override def show
   {
+    component.setLocation(location)
+    component.setSize(size)
+    component.setPreferredSize(size)
     component.setOpaque(true)
     layered.add(component, JLayeredPane.POPUP_LAYER)
+    layered.moveToFront(component)
     layered.repaint(component.getBounds())
   }
 

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/pretty_tooltip.scala
     Author:     Makarius
 
-Enhanced tooltip window based on Pretty_Text_Area.
+Tooltip based on Pretty_Text_Area.
 */
 
 package isabelle.jedit
@@ -11,7 +11,7 @@
 
 import java.awt.{Color, Point, BorderLayout, Dimension}
 import java.awt.event.{FocusAdapter, FocusEvent}
-import javax.swing.{JPanel, JComponent, PopupFactory}
+import javax.swing.{JPanel, JComponent, SwingUtilities}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
@@ -39,8 +39,8 @@
   def apply(
     view: View,
     parent: JComponent,
+    location: Point,
     rendering: Rendering,
-    screen_point: Point,
     results: Command.Results,
     info: Text.Info[XML.Body]): Pretty_Tooltip =
   {
@@ -56,7 +56,8 @@
           }
         old.foreach(_.hide_popup)
 
-        val tip = new Pretty_Tooltip(view, rendering, screen_point, results, info)
+        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
@@ -138,8 +139,8 @@
 
 class Pretty_Tooltip private(
   view: View,
+  location: Point,
   rendering: Rendering,
-  screen_point: Point,
   private val results: Command.Results,
   private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout)
 {
@@ -217,15 +218,9 @@
 
   private val popup =
   {
-    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
-
-    val root = view.getRootPane
-    val x0 = root.getLocationOnScreen.x
-    val y0 = root.getLocationOnScreen.y
-    val w0 = root.getWidth
-    val h0 = root.getHeight
-
-    val (w, h) =
+    val layered = view.getLayeredPane
+    val screen = JEdit_Lib.screen_location(layered, location)
+    val size =
     {
       val painter = pretty_text_area.getPainter
       val metric = JEdit_Lib.pretty_metric(painter)
@@ -239,8 +234,9 @@
       val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
       val bounds = Rendering.popup_bounds
 
+      val h0 = layered.getHeight
       val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
-      val h2 = h0 min (screen_bounds.height * bounds).toInt
+      val h2 = h0 min (screen.bounds.height * bounds).toInt
       val h = h1 min h2
 
       val margin1 =
@@ -248,25 +244,14 @@
           (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
         else margin
 
+      val w0 = layered.getWidth
       val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
-      val w2 = w0 min (screen_bounds.width * bounds).toInt
+      val w2 = w0 min (screen.bounds.width * bounds).toInt
       val w = w1 min w2
 
-      (w, h)
+      new Dimension(w, h)
     }
-
-    val (x, y) =
-    {
-      val x1 = x0 + w0 - w
-      val y1 = y0 + h0 - h
-      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
-      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
-      ((x2 min x1) max x0, (y2 min y1) max y0)
-    }
-
-    tip.setSize(new Dimension(w, h))
-    tip.setPreferredSize(new Dimension(w, h))
-    PopupFactory.getSharedInstance.getPopup(root, tip, x, y)
+    new Popup(layered, tip, screen.relative(layered, size), size)
   }
 
   private def show_popup

--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 28 15:14:58 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 28 16:36:46 2013 +0200
@@ -208,10 +208,9 @@
                       case None =>
                       case Some(tip) =>
                         val painter = text_area.getPainter
-                        val screen_point = evt.getLocationOnScreen
-                        screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
+                        val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
                         val results = rendering.command_results(range)
-                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip)
+                        Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                     }
                 }
               }