src/Tools/jEdit/src/completion_popup.scala
changeset 53246 8d34caf5bf82
parent 53244 ec6011bf2362
child 53247 bd595338ca18
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 10:35:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 15:14:58 2013 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Tools/jEdit/src/completion_popup.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Completion popup based on javax.swing.PopupFactory.
     1.8 +Completion popup.
     1.9  */
    1.10  
    1.11  package isabelle.jedit
    1.12 @@ -11,7 +11,7 @@
    1.13  
    1.14  import java.awt.{Font, Point, BorderLayout, Dimension}
    1.15  import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
    1.16 -import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
    1.17 +import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    1.18  
    1.19  import scala.swing.{ListView, ScrollPane}
    1.20  import scala.swing.event.MouseClicked
    1.21 @@ -28,29 +28,27 @@
    1.22    { override def toString: String = description }
    1.23  
    1.24  
    1.25 -  /* single instance within root */
    1.26 +  /* maintain single instance */
    1.27  
    1.28 -  def dismissed_view(view: View): Boolean = dismissed(view.getRootPane)
    1.29 -
    1.30 -  private def dismissed(root: JComponent): Boolean =
    1.31 +  def dismissed(layered: JLayeredPane): Boolean =
    1.32    {
    1.33      Swing_Thread.require()
    1.34  
    1.35 -    root.getClientProperty(Completion_Popup) match {
    1.36 +    layered.getClientProperty(Completion_Popup) match {
    1.37        case old_completion: Completion_Popup =>
    1.38 -        old_completion.hide_popup
    1.39 +        old_completion.hide_popup()
    1.40          true
    1.41        case _ =>
    1.42          false
    1.43      }
    1.44    }
    1.45  
    1.46 -  private def register(root: JComponent, completion: Completion_Popup)
    1.47 +  private def register(layered: JLayeredPane, completion: Completion_Popup)
    1.48    {
    1.49      Swing_Thread.require()
    1.50  
    1.51 -    dismissed(root)
    1.52 -    root.putClientProperty(Completion_Popup, completion)
    1.53 +    dismissed(layered)
    1.54 +    layered.putClientProperty(Completion_Popup, completion)
    1.55    }
    1.56  
    1.57  
    1.58 @@ -81,14 +79,14 @@
    1.59      {
    1.60        Swing_Thread.require()
    1.61  
    1.62 -      dismissed(text_area)
    1.63 -
    1.64        val view = text_area.getView
    1.65 -      val root = view.getRootPane
    1.66 +      val layered = view.getLayeredPane
    1.67        val buffer = text_area.getBuffer
    1.68        val painter = text_area.getPainter
    1.69  
    1.70        if (buffer.isEditable && !evt.isConsumed) {
    1.71 +        dismissed(layered)
    1.72 +
    1.73          get_syntax match {
    1.74            case Some(syntax) =>
    1.75              val caret = text_area.getCaretPosition
    1.76 @@ -116,13 +114,13 @@
    1.77                      (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    1.78                        max 10.0f)
    1.79  
    1.80 -                val location = text_area.offsetToXY(caret - original.length)
    1.81 -                if (location != null) {
    1.82 -                  location.y = location.y + painter.getFontMetrics.getHeight
    1.83 -                  SwingUtilities.convertPointToScreen(location, painter)
    1.84 -
    1.85 +                val loc1 = text_area.offsetToXY(caret - original.length)
    1.86 +                if (loc1 != null) {
    1.87 +                  val loc2 =
    1.88 +                    SwingUtilities.convertPoint(painter,
    1.89 +                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.90                    val completion =
    1.91 -                    new Completion_Popup(root, popup_font, location, items) {
    1.92 +                    new Completion_Popup(layered, loc2, popup_font, items) {
    1.93                        override def complete(item: Item) { insert(text_area, item) }
    1.94                        override def propagate(e: KeyEvent) {
    1.95                          JEdit_Lib.propagate_key(view, e)
    1.96 @@ -130,7 +128,8 @@
    1.97                        }
    1.98                        override def refocus() { text_area.requestFocus }
    1.99                      }
   1.100 -                  register(root, completion)
   1.101 +                  register(layered, completion)
   1.102 +                  completion.show_popup()
   1.103                  }
   1.104                case None =>
   1.105              }
   1.106 @@ -143,9 +142,9 @@
   1.107  
   1.108  
   1.109  class Completion_Popup private(
   1.110 -  root: JComponent,
   1.111 +  layered: JLayeredPane,
   1.112 +  location: Point,
   1.113    popup_font: Font,
   1.114 -  screen_point: Point,
   1.115    items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
   1.116  {
   1.117    completion =>
   1.118 @@ -250,12 +249,12 @@
   1.119  
   1.120    private val popup =
   1.121    {
   1.122 +    val screen_point = new Point(location.x, location.y)
   1.123 +    SwingUtilities.convertPointToScreen(screen_point, layered)
   1.124      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
   1.125  
   1.126 -    val x0 = root.getLocationOnScreen.x
   1.127 -    val y0 = root.getLocationOnScreen.y
   1.128 -    val w0 = root.getWidth
   1.129 -    val h0 = root.getHeight
   1.130 +    val w0 = layered.getWidth
   1.131 +    val h0 = layered.getHeight
   1.132  
   1.133      val (w, h) =
   1.134      {
   1.135 @@ -268,16 +267,29 @@
   1.136  
   1.137      val (x, y) =
   1.138      {
   1.139 +      val x0 = layered.getLocationOnScreen.x
   1.140 +      val y0 = layered.getLocationOnScreen.y
   1.141        val x1 = x0 + w0 - w
   1.142        val y1 = y0 + h0 - h
   1.143        val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
   1.144        val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
   1.145 -      ((x2 min x1) max x0, (y2 min y1) max y0)
   1.146 +
   1.147 +      val point = new Point((x2 min x1) max x0, (y2 min y1) max y0)
   1.148 +      SwingUtilities.convertPointFromScreen(point, layered)
   1.149 +      (point.x, point.y)
   1.150      }
   1.151  
   1.152 +    completion.setLocation(x, y)
   1.153      completion.setSize(new Dimension(w, h))
   1.154      completion.setPreferredSize(new Dimension(w, h))
   1.155 -    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
   1.156 +
   1.157 +    new Popup(layered, completion)
   1.158 +  }
   1.159 +
   1.160 +  private def show_popup()
   1.161 +  {
   1.162 +    popup.show
   1.163 +    list_view.requestFocus
   1.164    }
   1.165  
   1.166    private def hide_popup()
   1.167 @@ -286,8 +298,5 @@
   1.168      popup.hide
   1.169      if (had_focus) refocus()
   1.170    }
   1.171 -
   1.172 -  popup.show
   1.173 -  list_view.requestFocus
   1.174  }
   1.175