# HG changeset patch
# User wenzelm
# Date 1377695698 -7200
# Node ID 8d34caf5bf8211c81b5d469598a5cdd90e16513c
# Parent  301b69957af7bc84613f374e85ce300dca994646
more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
observe !evt.isConsumed semantically: no initial dismiss here (e.g. due to cursor keys);

diff -r 301b69957af7 -r 8d34caf5bf82 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 28 10:35:12 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 28 15:14:58 2013 +0200
@@ -33,6 +33,7 @@
   "src/osx_adapter.scala"
   "src/output_dockable.scala"
   "src/plugin.scala"
+  "src/popup.scala"
   "src/pretty_text_area.scala"
   "src/pretty_tooltip.scala"
   "src/process_indicator.scala"
diff -r 301b69957af7 -r 8d34caf5bf82 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 10:35:12 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 15:14:58 2013 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/completion_popup.scala
     Author:     Makarius
 
-Completion popup based on javax.swing.PopupFactory.
+Completion popup.
 */
 
 package isabelle.jedit
@@ -11,7 +11,7 @@
 
 import java.awt.{Font, Point, BorderLayout, Dimension}
 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
-import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
+import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
@@ -28,29 +28,27 @@
   { override def toString: String = description }
 
 
-  /* single instance within root */
+  /* maintain single instance */
 
-  def dismissed_view(view: View): Boolean = dismissed(view.getRootPane)
-
-  private def dismissed(root: JComponent): Boolean =
+  def dismissed(layered: JLayeredPane): Boolean =
   {
     Swing_Thread.require()
 
-    root.getClientProperty(Completion_Popup) match {
+    layered.getClientProperty(Completion_Popup) match {
       case old_completion: Completion_Popup =>
-        old_completion.hide_popup
+        old_completion.hide_popup()
         true
       case _ =>
         false
     }
   }
 
-  private def register(root: JComponent, completion: Completion_Popup)
+  private def register(layered: JLayeredPane, completion: Completion_Popup)
   {
     Swing_Thread.require()
 
-    dismissed(root)
-    root.putClientProperty(Completion_Popup, completion)
+    dismissed(layered)
+    layered.putClientProperty(Completion_Popup, completion)
   }
 
 
@@ -81,14 +79,14 @@
     {
       Swing_Thread.require()
 
-      dismissed(text_area)
-
       val view = text_area.getView
-      val root = view.getRootPane
+      val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
       if (buffer.isEditable && !evt.isConsumed) {
+        dismissed(layered)
+
         get_syntax match {
           case Some(syntax) =>
             val caret = text_area.getCaretPosition
@@ -116,13 +114,13 @@
                     (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
                       max 10.0f)
 
-                val location = text_area.offsetToXY(caret - original.length)
-                if (location != null) {
-                  location.y = location.y + painter.getFontMetrics.getHeight
-                  SwingUtilities.convertPointToScreen(location, painter)
-
+                val loc1 = text_area.offsetToXY(caret - original.length)
+                if (loc1 != null) {
+                  val loc2 =
+                    SwingUtilities.convertPoint(painter,
+                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
                   val completion =
-                    new Completion_Popup(root, popup_font, location, items) {
+                    new Completion_Popup(layered, loc2, popup_font, items) {
                       override def complete(item: Item) { insert(text_area, item) }
                       override def propagate(e: KeyEvent) {
                         JEdit_Lib.propagate_key(view, e)
@@ -130,7 +128,8 @@
                       }
                       override def refocus() { text_area.requestFocus }
                     }
-                  register(root, completion)
+                  register(layered, completion)
+                  completion.show_popup()
                 }
               case None =>
             }
@@ -143,9 +142,9 @@
 
 
 class Completion_Popup private(
-  root: JComponent,
+  layered: JLayeredPane,
+  location: Point,
   popup_font: Font,
-  screen_point: Point,
   items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
 {
   completion =>
@@ -250,12 +249,12 @@
 
   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 x0 = root.getLocationOnScreen.x
-    val y0 = root.getLocationOnScreen.y
-    val w0 = root.getWidth
-    val h0 = root.getHeight
+    val w0 = layered.getWidth
+    val h0 = layered.getHeight
 
     val (w, h) =
     {
@@ -268,16 +267,29 @@
 
     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)
-      ((x2 min x1) max x0, (y2 min y1) max y0)
+
+      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))
-    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
+
+    new Popup(layered, completion)
+  }
+
+  private def show_popup()
+  {
+    popup.show
+    list_view.requestFocus
   }
 
   private def hide_popup()
@@ -286,8 +298,5 @@
     popup.hide
     if (had_focus) refocus()
   }
-
-  popup.show
-  list_view.requestFocus
 }
 
diff -r 301b69957af7 -r 8d34caf5bf82 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 10:35:12 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 15:14:58 2013 +0200
@@ -57,7 +57,7 @@
 
   def dismissed_popups(view: View): Boolean =
   {
-    val b1 = Completion_Popup.dismissed_view(view)
+    val b1 = Completion_Popup.dismissed(view.getLayeredPane)
     val b2 = Pretty_Tooltip.dismissed_all()
     b1 || b2
   }
diff -r 301b69957af7 -r 8d34caf5bf82 src/Tools/jEdit/src/popup.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/popup.scala	Wed Aug 28 15:14:58 2013 +0200
@@ -0,0 +1,33 @@
+/*  Title:      Tools/jEdit/src/popup.scala
+    Author:     Makarius
+
+Simple popup within layered pane, based on component with given geometry.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import javax.swing.{JLayeredPane, JComponent}
+
+
+class Popup(
+  layered: JLayeredPane,
+  component: JComponent) extends javax.swing.Popup()
+{
+  override def show
+  {
+    component.setOpaque(true)
+    layered.add(component, JLayeredPane.POPUP_LAYER)
+    layered.repaint(component.getBounds())
+  }
+
+  override def hide
+  {
+    val bounds = component.getBounds()
+    layered.remove(component)
+    layered.repaint(bounds)
+  }
+}
+