src/Tools/jEdit/etc/options
changeset 56197 416f7a00e4cb
parent 56170 638b29331549
child 56202 0a11d17eeeff
equal deleted inserted replaced
56187:2666cd7d380c 56197:416f7a00e4cb
    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.5
    45 public option jedit_completion_delay : real = 0.5
    46   -- "delay for completion popup (seconds)"
    46   -- "delay for completion popup (seconds)"
    47 
       
    48 public option jedit_completion_dismiss_delay : real = 0.0
       
    49   -- "delay for dismissing obsolete completion popup (seconds)"
       
    50 
    47 
    51 public option jedit_completion_immediate : bool = false
    48 public option jedit_completion_immediate : bool = false
    52   -- "insert unique completion immediately into buffer (if delay = 0)"
    49   -- "insert unique completion immediately into buffer (if delay = 0)"
    53 
    50 
    54 
    51