etc/options
changeset 73173 fbc1d5ff3683
parent 73129 d15c0c7ae092
child 73251 4519ba8da368
equal deleted inserted replaced
73172:f7954a960890 73173:fbc1d5ff3683
   157 section "Editor Session"
   157 section "Editor Session"
   158 
   158 
   159 public option editor_load_delay : real = 0.5
   159 public option editor_load_delay : real = 0.5
   160   -- "delay for file load operations (new buffers etc.)"
   160   -- "delay for file load operations (new buffers etc.)"
   161 
   161 
   162 public option editor_input_delay : real = 0.3
   162 public option editor_input_delay : real = 0.2
   163   -- "delay for user input (text edits, cursor movement etc.)"
   163   -- "delay for user input (text edits, cursor movement etc.)"
   164 
   164 
   165 public option editor_generated_input_delay : real = 1.0
   165 public option editor_generated_input_delay : real = 1.0
   166   -- "delay for machine-generated input that may outperform user edits"
   166   -- "delay for machine-generated input that may outperform user edits"
   167 
   167