more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
authorwenzelm
Wed Aug 28 15:14:58 2013 +0200 (2013-08-28 ago)
changeset 532468d34caf5bf82
parent 53245 301b69957af7
child 53247 bd595338ca18
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);
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/popup.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 28 10:35:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 28 15:14:58 2013 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    "src/osx_adapter.scala"
     1.5    "src/output_dockable.scala"
     1.6    "src/plugin.scala"
     1.7 +  "src/popup.scala"
     1.8    "src/pretty_text_area.scala"
     1.9    "src/pretty_tooltip.scala"
    1.10    "src/process_indicator.scala"
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 10:35:12 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 15:14:58 2013 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Tools/jEdit/src/completion_popup.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Completion popup based on javax.swing.PopupFactory.
     2.8 +Completion popup.
     2.9  */
    2.10  
    2.11  package isabelle.jedit
    2.12 @@ -11,7 +11,7 @@
    2.13  
    2.14  import java.awt.{Font, Point, BorderLayout, Dimension}
    2.15  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
    2.16 -import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
    2.17 +import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    2.18  
    2.19  import scala.swing.{ListView, ScrollPane}
    2.20  import scala.swing.event.MouseClicked
    2.21 @@ -28,29 +28,27 @@
    2.22    { override def toString: String = description }
    2.23  
    2.24  
    2.25 -  /* single instance within root */
    2.26 +  /* maintain single instance */
    2.27  
    2.28 -  def dismissed_view(view: View): Boolean = dismissed(view.getRootPane)
    2.29 -
    2.30 -  private def dismissed(root: JComponent): Boolean =
    2.31 +  def dismissed(layered: JLayeredPane): Boolean =
    2.32    {
    2.33      Swing_Thread.require()
    2.34  
    2.35 -    root.getClientProperty(Completion_Popup) match {
    2.36 +    layered.getClientProperty(Completion_Popup) match {
    2.37        case old_completion: Completion_Popup =>
    2.38 -        old_completion.hide_popup
    2.39 +        old_completion.hide_popup()
    2.40          true
    2.41        case _ =>
    2.42          false
    2.43      }
    2.44    }
    2.45  
    2.46 -  private def register(root: JComponent, completion: Completion_Popup)
    2.47 +  private def register(layered: JLayeredPane, completion: Completion_Popup)
    2.48    {
    2.49      Swing_Thread.require()
    2.50  
    2.51 -    dismissed(root)
    2.52 -    root.putClientProperty(Completion_Popup, completion)
    2.53 +    dismissed(layered)
    2.54 +    layered.putClientProperty(Completion_Popup, completion)
    2.55    }
    2.56  
    2.57  
    2.58 @@ -81,14 +79,14 @@
    2.59      {
    2.60        Swing_Thread.require()
    2.61  
    2.62 -      dismissed(text_area)
    2.63 -
    2.64        val view = text_area.getView
    2.65 -      val root = view.getRootPane
    2.66 +      val layered = view.getLayeredPane
    2.67        val buffer = text_area.getBuffer
    2.68        val painter = text_area.getPainter
    2.69  
    2.70        if (buffer.isEditable && !evt.isConsumed) {
    2.71 +        dismissed(layered)
    2.72 +
    2.73          get_syntax match {
    2.74            case Some(syntax) =>
    2.75              val caret = text_area.getCaretPosition
    2.76 @@ -116,13 +114,13 @@
    2.77                      (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    2.78                        max 10.0f)
    2.79  
    2.80 -                val location = text_area.offsetToXY(caret - original.length)
    2.81 -                if (location != null) {
    2.82 -                  location.y = location.y + painter.getFontMetrics.getHeight
    2.83 -                  SwingUtilities.convertPointToScreen(location, painter)
    2.84 -
    2.85 +                val loc1 = text_area.offsetToXY(caret - original.length)
    2.86 +                if (loc1 != null) {
    2.87 +                  val loc2 =
    2.88 +                    SwingUtilities.convertPoint(painter,
    2.89 +                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    2.90                    val completion =
    2.91 -                    new Completion_Popup(root, popup_font, location, items) {
    2.92 +                    new Completion_Popup(layered, loc2, popup_font, items) {
    2.93                        override def complete(item: Item) { insert(text_area, item) }
    2.94                        override def propagate(e: KeyEvent) {
    2.95                          JEdit_Lib.propagate_key(view, e)
    2.96 @@ -130,7 +128,8 @@
    2.97                        }
    2.98                        override def refocus() { text_area.requestFocus }
    2.99                      }
   2.100 -                  register(root, completion)
   2.101 +                  register(layered, completion)
   2.102 +                  completion.show_popup()
   2.103                  }
   2.104                case None =>
   2.105              }
   2.106 @@ -143,9 +142,9 @@
   2.107  
   2.108  
   2.109  class Completion_Popup private(
   2.110 -  root: JComponent,
   2.111 +  layered: JLayeredPane,
   2.112 +  location: Point,
   2.113    popup_font: Font,
   2.114 -  screen_point: Point,
   2.115    items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
   2.116  {
   2.117    completion =>
   2.118 @@ -250,12 +249,12 @@
   2.119  
   2.120    private val popup =
   2.121    {
   2.122 +    val screen_point = new Point(location.x, location.y)
   2.123 +    SwingUtilities.convertPointToScreen(screen_point, layered)
   2.124      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
   2.125  
   2.126 -    val x0 = root.getLocationOnScreen.x
   2.127 -    val y0 = root.getLocationOnScreen.y
   2.128 -    val w0 = root.getWidth
   2.129 -    val h0 = root.getHeight
   2.130 +    val w0 = layered.getWidth
   2.131 +    val h0 = layered.getHeight
   2.132  
   2.133      val (w, h) =
   2.134      {
   2.135 @@ -268,16 +267,29 @@
   2.136  
   2.137      val (x, y) =
   2.138      {
   2.139 +      val x0 = layered.getLocationOnScreen.x
   2.140 +      val y0 = layered.getLocationOnScreen.y
   2.141        val x1 = x0 + w0 - w
   2.142        val y1 = y0 + h0 - h
   2.143        val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
   2.144        val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
   2.145 -      ((x2 min x1) max x0, (y2 min y1) max y0)
   2.146 +
   2.147 +      val point = new Point((x2 min x1) max x0, (y2 min y1) max y0)
   2.148 +      SwingUtilities.convertPointFromScreen(point, layered)
   2.149 +      (point.x, point.y)
   2.150      }
   2.151  
   2.152 +    completion.setLocation(x, y)
   2.153      completion.setSize(new Dimension(w, h))
   2.154      completion.setPreferredSize(new Dimension(w, h))
   2.155 -    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
   2.156 +
   2.157 +    new Popup(layered, completion)
   2.158 +  }
   2.159 +
   2.160 +  private def show_popup()
   2.161 +  {
   2.162 +    popup.show
   2.163 +    list_view.requestFocus
   2.164    }
   2.165  
   2.166    private def hide_popup()
   2.167 @@ -286,8 +298,5 @@
   2.168      popup.hide
   2.169      if (had_focus) refocus()
   2.170    }
   2.171 -
   2.172 -  popup.show
   2.173 -  list_view.requestFocus
   2.174  }
   2.175  
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 10:35:12 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 15:14:58 2013 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4  
     3.5    def dismissed_popups(view: View): Boolean =
     3.6    {
     3.7 -    val b1 = Completion_Popup.dismissed_view(view)
     3.8 +    val b1 = Completion_Popup.dismissed(view.getLayeredPane)
     3.9      val b2 = Pretty_Tooltip.dismissed_all()
    3.10      b1 || b2
    3.11    }
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/popup.scala	Wed Aug 28 15:14:58 2013 +0200
     4.3 @@ -0,0 +1,33 @@
     4.4 +/*  Title:      Tools/jEdit/src/popup.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Simple popup within layered pane, based on component with given geometry.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.jedit
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +import javax.swing.{JLayeredPane, JComponent}
    4.16 +
    4.17 +
    4.18 +class Popup(
    4.19 +  layered: JLayeredPane,
    4.20 +  component: JComponent) extends javax.swing.Popup()
    4.21 +{
    4.22 +  override def show
    4.23 +  {
    4.24 +    component.setOpaque(true)
    4.25 +    layered.add(component, JLayeredPane.POPUP_LAYER)
    4.26 +    layered.repaint(component.getBounds())
    4.27 +  }
    4.28 +
    4.29 +  override def hide
    4.30 +  {
    4.31 +    val bounds = component.getBounds()
    4.32 +    layered.remove(component)
    4.33 +    layered.repaint(bounds)
    4.34 +  }
    4.35 +}
    4.36 +