equal
deleted
inserted
replaced
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 |