src/Tools/jEdit/etc/options

 
 option jedit_tooltip_font_size : int = 10
   -- "tooltip font size (according to HTML)"
 
 option jedit_tooltip_margin : int = 60
-  -- "margin for tooltip pretty-printing (in characters)"
+  -- "margin for tooltip pretty-printing"
 
 option jedit_tooltip_dismiss_delay : real = 8.0
-  -- "global delay for Swing tooltips (in seconds)"
+  -- "global delay for Swing tooltips"
+
+option jedit_load_delay : real = 0.5
+  -- "delay for file load operations (new buffers etc.)"