src/Tools/jEdit/etc/options
changeset 56842 b6e266574b26
parent 56597 f4f561bf4b07
child 56843 b2bfcd8cda80
equal deleted inserted replaced
56841:bc6faeadbf82 56842:b6e266574b26
    39 
    39 
    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 
       
    45 public option jedit_completion_context : bool = true
       
    46   -- "use semantic language context for completion"
    44 
    47 
    45 public option jedit_completion_delay : real = 0.5
    48 public option jedit_completion_delay : real = 0.5
    46   -- "delay for completion popup (seconds)"
    49   -- "delay for completion popup (seconds)"
    47 
    50 
    48 public option jedit_completion_immediate : bool = false
    51 public option jedit_completion_immediate : bool = false