equal
deleted
inserted
replaced
40 section "Completion" |
40 section "Completion" |
41 |
41 |
42 public option jedit_completion : bool = true |
42 public option jedit_completion : bool = true |
43 -- "enable completion popup" |
43 -- "enable completion popup" |
44 |
44 |
45 public option jedit_completion_delay : real = 0.0 |
45 public option jedit_completion_delay : real = 0.5 |
46 -- "delay for completion popup (seconds)" |
46 -- "delay for completion popup (seconds)" |
47 |
47 |
48 public option jedit_completion_dismiss_delay : real = 0.0 |
48 public option jedit_completion_dismiss_delay : real = 0.0 |
49 -- "delay for dismissing obsolete completion popup (seconds)" |
49 -- "delay for dismissing obsolete completion popup (seconds)" |
50 |
50 |