src/Tools/jEdit/src/completion_popup.scala
changeset 53230 6589ff56cc3c
parent 53229 6ce8328d7912
child 53231 423e29f1f304
equal deleted inserted replaced
53229:6ce8328d7912 53230:6589ff56cc3c
   201 
   201 
   202   private val popup =
   202   private val popup =
   203   {
   203   {
   204     val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
   204     val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
   205 
   205 
   206     val geometry = JEdit_Lib.window_geometry(completion, completion)
   206     val x0 = root.getLocationOnScreen.x
   207 
   207     val y0 = root.getLocationOnScreen.y
   208     val w = geometry.width min (screen_bounds.width / 2)
   208     val w0 = root.getWidth
   209     val h = geometry.height min (screen_bounds.height / 2)
   209     val h0 = root.getHeight
       
   210 
       
   211     val (w, h) =
       
   212     {
       
   213       val geometry = JEdit_Lib.window_geometry(completion, completion)
       
   214       val bounds = Rendering.popup_bounds
       
   215       val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
       
   216       val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
       
   217       (w, h)
       
   218     }
       
   219 
       
   220     val (x, y) =
       
   221     {
       
   222       val x1 = x0 + w0 - w
       
   223       val y1 = y0 + h0 - h
       
   224       val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
       
   225       val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
       
   226       ((x2 min x1) max x0, (y2 min y1) max y0)
       
   227     }
   210 
   228 
   211     completion.setSize(new Dimension(w, h))
   229     completion.setSize(new Dimension(w, h))
   212     completion.setPreferredSize(new Dimension(w, h))
   230     completion.setPreferredSize(new Dimension(w, h))
   213 
       
   214     val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
       
   215     val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
       
   216     PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
   231     PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
   217   }
   232   }
   218 
   233 
   219   def show_popup()
   234   def show_popup()
   220   {
   235   {