equal
deleted
inserted
replaced
123 -- "delay for user input (text edits, cursor movement etc.)" |
123 -- "delay for user input (text edits, cursor movement etc.)" |
124 |
124 |
125 public option editor_output_delay : real = 0.1 |
125 public option editor_output_delay : real = 0.1 |
126 -- "delay for prover output (markup, common messages etc.)" |
126 -- "delay for prover output (markup, common messages etc.)" |
127 |
127 |
128 public option editor_prune_delay : real = 30.0 |
128 public option editor_prune_delay : real = 15 |
129 -- "delay to prune history (delete old versions)" |
129 -- "delay to prune history (delete old versions)" |
130 |
130 |
131 public option editor_update_delay : real = 0.5 |
131 public option editor_update_delay : real = 0.5 |
132 -- "delay for physical GUI updates" |
132 -- "delay for physical GUI updates" |
133 |
133 |