# HG changeset patch # User wenzelm # Date 1377612568 -7200 # Node ID 6589ff56cc3c64c65c3aec39f9ca8107ce805047 # Parent 6ce8328d79123e6cc24c2bfa18aa91342bfa79f0 determine completion geometry like tooltip; just one option jedit_popup_bounds for tooltip and completion; diff -r 6ce8328d7912 -r 6589ff56cc3c src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Aug 27 15:35:51 2013 +0200 +++ b/src/Tools/jEdit/etc/options Tue Aug 27 16:09:28 2013 +0200 @@ -12,15 +12,15 @@ public option jedit_popup_font_scale : real = 0.85 -- "scale factor of popups wrt. main text area" +public option jedit_popup_bounds : real = 0.5 + -- "relative bounds of popup window wrt. logical screen size" + public option jedit_tooltip_delay : real = 0.75 -- "open/close delay for document tooltips" public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" -public option jedit_tooltip_bounds : real = 0.5 - -- "relative bounds of tooltip window wrt. logical screen size" - public option jedit_text_overview_limit : int = 100000 -- "maximum amount of text to visualize in overview column" diff -r 6ce8328d7912 -r 6589ff56cc3c src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 15:35:51 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 16:09:28 2013 +0200 @@ -203,16 +203,31 @@ { val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - val geometry = JEdit_Lib.window_geometry(completion, completion) + val x0 = root.getLocationOnScreen.x + val y0 = root.getLocationOnScreen.y + val w0 = root.getWidth + val h0 = root.getHeight - val w = geometry.width min (screen_bounds.width / 2) - val h = geometry.height min (screen_bounds.height / 2) + val (w, h) = + { + val geometry = JEdit_Lib.window_geometry(completion, completion) + val bounds = Rendering.popup_bounds + val w = geometry.width min (screen_bounds.width * bounds).toInt min w0 + val h = geometry.height min (screen_bounds.height * bounds).toInt min h0 + (w, h) + } + + val (x, y) = + { + val x1 = x0 + w0 - w + val y1 = y0 + h0 - h + val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w) + val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h) + ((x2 min x1) max x0, (y2 min y1) max y0) + } completion.setSize(new Dimension(w, h)) completion.setPreferredSize(new Dimension(w, h)) - - val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w) - val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h) PopupFactory.getSharedInstance.getPopup(root, completion, x, y) } diff -r 6ce8328d7912 -r 6589ff56cc3c src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 27 15:35:51 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 27 16:09:28 2013 +0200 @@ -237,7 +237,7 @@ (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter) - val bounds = rendering.tooltip_bounds + val bounds = Rendering.popup_bounds val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height val h2 = h0 min (screen_bounds.height * bounds).toInt diff -r 6ce8328d7912 -r 6589ff56cc3c src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Aug 27 15:35:51 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Tue Aug 27 16:09:28 2013 +0200 @@ -49,6 +49,11 @@ (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat + /* popup window bounds */ + + def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 + + /* token markup -- text styles */ private val command_style: Map[String, Byte] = @@ -372,7 +377,6 @@ } val tooltip_margin: Int = options.int("jedit_tooltip_margin") - val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8 lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))