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 { |