equal
deleted
inserted
replaced
172 |
172 |
173 public option editor_reparse_limit : int = 10000 |
173 public option editor_reparse_limit : int = 10000 |
174 -- "maximum amount of reparsed text outside perspective" |
174 -- "maximum amount of reparsed text outside perspective" |
175 |
175 |
176 public option editor_tracing_messages : int = 1000 |
176 public option editor_tracing_messages : int = 1000 |
177 -- "initial number of tracing messages for each command transaction" |
177 -- "initial number of tracing messages for each command transaction (0: unbounded)" |
178 |
178 |
179 public option editor_chart_delay : real = 3.0 |
179 public option editor_chart_delay : real = 3.0 |
180 -- "delay for chart repainting" |
180 -- "delay for chart repainting" |
181 |
181 |
182 public option editor_continuous_checking : bool = true |
182 public option editor_continuous_checking : bool = true |