src/Tools/jEdit/src/completion_popup.scala
changeset 53230 6589ff56cc3c
parent 53229 6ce8328d7912
child 53231 423e29f1f304
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 15:35:51 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:09:28 2013 +0200
     1.3 @@ -203,16 +203,31 @@
     1.4    {
     1.5      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
     1.6  
     1.7 -    val geometry = JEdit_Lib.window_geometry(completion, completion)
     1.8 +    val x0 = root.getLocationOnScreen.x
     1.9 +    val y0 = root.getLocationOnScreen.y
    1.10 +    val w0 = root.getWidth
    1.11 +    val h0 = root.getHeight
    1.12  
    1.13 -    val w = geometry.width min (screen_bounds.width / 2)
    1.14 -    val h = geometry.height min (screen_bounds.height / 2)
    1.15 +    val (w, h) =
    1.16 +    {
    1.17 +      val geometry = JEdit_Lib.window_geometry(completion, completion)
    1.18 +      val bounds = Rendering.popup_bounds
    1.19 +      val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
    1.20 +      val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
    1.21 +      (w, h)
    1.22 +    }
    1.23 +
    1.24 +    val (x, y) =
    1.25 +    {
    1.26 +      val x1 = x0 + w0 - w
    1.27 +      val y1 = y0 + h0 - h
    1.28 +      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    1.29 +      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    1.30 +      ((x2 min x1) max x0, (y2 min y1) max y0)
    1.31 +    }
    1.32  
    1.33      completion.setSize(new Dimension(w, h))
    1.34      completion.setPreferredSize(new Dimension(w, h))
    1.35 -
    1.36 -    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    1.37 -    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    1.38      PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
    1.39    }
    1.40