determine completion geometry like tooltip;
authorwenzelm
Tue, 27 Aug 2013 16:09:28 +0200
changeset 53230 6589ff56cc3c
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
--- 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"
 
--- 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)
   }
 
--- 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
--- 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"))