equal
deleted
inserted
replaced
115 -- "delay for user input (text edits, cursor movement etc.)" |
115 -- "delay for user input (text edits, cursor movement etc.)" |
116 |
116 |
117 public option editor_output_delay : real = 0.1 |
117 public option editor_output_delay : real = 0.1 |
118 -- "delay for prover output (markup, common messages etc.)" |
118 -- "delay for prover output (markup, common messages etc.)" |
119 |
119 |
|
120 public option editor_prune_delay : real = 60.0 |
|
121 -- "delay to prune history (delete old versions)" |
|
122 |
120 public option editor_update_delay : real = 0.5 |
123 public option editor_update_delay : real = 0.5 |
121 -- "delay for physical GUI updates" |
124 -- "delay for physical GUI updates" |
122 |
125 |
123 public option editor_reparse_limit : int = 10000 |
126 public option editor_reparse_limit : int = 10000 |
124 -- "maximum amount of reparsed text outside perspective" |
127 -- "maximum amount of reparsed text outside perspective" |