equal
deleted
inserted
replaced
121 -- "initial number of tracing messages for each command transaction" |
121 -- "initial number of tracing messages for each command transaction" |
122 |
122 |
123 public option editor_chart_delay : real = 3.0 |
123 public option editor_chart_delay : real = 3.0 |
124 -- "delay for chart repainting" |
124 -- "delay for chart repainting" |
125 |
125 |
|
126 option editor_execution_delay : real = 0.02 |
|
127 -- "delay for start of execution process after document update (seconds)" |
|
128 |
126 option editor_execution_priority : int = -1 |
129 option editor_execution_priority : int = -1 |
127 -- "execution priority of main document structure (e.g. 0, -1, -2)" |
130 -- "execution priority of main document structure (e.g. 0, -1, -2)" |
128 |
131 |
129 option editor_execution_range : string = "visible" |
132 option editor_execution_range : string = "visible" |
130 -- "execution range of continuous document processing: all, none, visible" |
133 -- "execution range of continuous document processing: all, none, visible" |