equal
deleted
inserted
replaced
92 -- "delay for physical GUI updates" |
92 -- "delay for physical GUI updates" |
93 |
93 |
94 option editor_reparse_limit : int = 10000 |
94 option editor_reparse_limit : int = 10000 |
95 -- "maximum amount of reparsed text outside perspective" |
95 -- "maximum amount of reparsed text outside perspective" |
96 |
96 |
97 option editor_tracing_messages : int = 100 |
97 option editor_tracing_messages : int = 1000 |
98 -- "initial number of tracing messages for each command transaction" |
98 -- "initial number of tracing messages for each command transaction" |
99 |
99 |
100 option editor_chart_delay : real = 3.0 |
100 option editor_chart_delay : real = 3.0 |
101 -- "delay for chart repainting" |
101 -- "delay for chart repainting" |