determine completion geometry like tooltip;
authorwenzelm
Tue Aug 27 16:09:28 2013 +0200 (2013-08-27 ago)
changeset 532306589ff56cc3c
parent 53229 6ce8328d7912
child 53231 423e29f1f304
determine completion geometry like tooltip;
just one option jedit_popup_bounds for tooltip and completion;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Tue Aug 27 15:35:51 2013 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Tue Aug 27 16:09:28 2013 +0200
     1.3 @@ -12,15 +12,15 @@
     1.4  public option jedit_popup_font_scale : real = 0.85
     1.5    -- "scale factor of popups wrt. main text area"
     1.6  
     1.7 +public option jedit_popup_bounds : real = 0.5
     1.8 +  -- "relative bounds of popup window wrt. logical screen size"
     1.9 +
    1.10  public option jedit_tooltip_delay : real = 0.75
    1.11    -- "open/close delay for document tooltips"
    1.12  
    1.13  public option jedit_tooltip_margin : int = 60
    1.14    -- "margin for tooltip pretty-printing"
    1.15  
    1.16 -public option jedit_tooltip_bounds : real = 0.5
    1.17 -  -- "relative bounds of tooltip window wrt. logical screen size"
    1.18 -
    1.19  public option jedit_text_overview_limit : int = 100000
    1.20    -- "maximum amount of text to visualize in overview column"
    1.21  
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 15:35:51 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:09:28 2013 +0200
     2.3 @@ -203,16 +203,31 @@
     2.4    {
     2.5      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
     2.6  
     2.7 -    val geometry = JEdit_Lib.window_geometry(completion, completion)
     2.8 +    val x0 = root.getLocationOnScreen.x
     2.9 +    val y0 = root.getLocationOnScreen.y
    2.10 +    val w0 = root.getWidth
    2.11 +    val h0 = root.getHeight
    2.12  
    2.13 -    val w = geometry.width min (screen_bounds.width / 2)
    2.14 -    val h = geometry.height min (screen_bounds.height / 2)
    2.15 +    val (w, h) =
    2.16 +    {
    2.17 +      val geometry = JEdit_Lib.window_geometry(completion, completion)
    2.18 +      val bounds = Rendering.popup_bounds
    2.19 +      val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
    2.20 +      val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
    2.21 +      (w, h)
    2.22 +    }
    2.23 +
    2.24 +    val (x, y) =
    2.25 +    {
    2.26 +      val x1 = x0 + w0 - w
    2.27 +      val y1 = y0 + h0 - h
    2.28 +      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    2.29 +      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    2.30 +      ((x2 min x1) max x0, (y2 min y1) max y0)
    2.31 +    }
    2.32  
    2.33      completion.setSize(new Dimension(w, h))
    2.34      completion.setPreferredSize(new Dimension(w, h))
    2.35 -
    2.36 -    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
    2.37 -    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
    2.38      PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
    2.39    }
    2.40  
     3.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 27 15:35:51 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 27 16:09:28 2013 +0200
     3.3 @@ -237,7 +237,7 @@
     3.4            (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
     3.5  
     3.6        val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
     3.7 -      val bounds = rendering.tooltip_bounds
     3.8 +      val bounds = Rendering.popup_bounds
     3.9  
    3.10        val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
    3.11        val h2 = h0 min (screen_bounds.height * bounds).toInt
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 27 15:35:51 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 27 16:09:28 2013 +0200
     4.3 @@ -49,6 +49,11 @@
     4.4      (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
     4.5  
     4.6  
     4.7 +  /* popup window bounds */
     4.8 +
     4.9 +  def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
    4.10 +
    4.11 +
    4.12    /* token markup -- text styles */
    4.13  
    4.14    private val command_style: Map[String, Byte] =
    4.15 @@ -372,7 +377,6 @@
    4.16    }
    4.17  
    4.18    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
    4.19 -  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
    4.20  
    4.21    lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
    4.22    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))