src/Tools/jEdit/etc/options

   -- "scale factor of add-on panels wrt. main text area"
 
 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"
 
 public option jedit_symbols_search_limit : int = 50