diff -r 0dfd78ff7696 -r 473ea1ed7503 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Aug 29 10:01:59 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 10:24:43 2013 +0200
@@ -16,7 +16,7 @@
   -- "relative bounds of popup window wrt. logical screen size"
 
 public option jedit_tooltip_delay : real = 0.75
-  -- "open/close delay for document tooltips"
+  -- "open/close delay for document tooltips (seconds)"
 
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
@@ -33,6 +33,12 @@
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
+public option jedit_completion : bool = true
+  -- "enable completion popup"
+
+public option jedit_completion_delay : real = 0.0
+  -- "delay for completion popup (seconds)"
+
 
 section "Rendering of Document Content"