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 public option editor_execution_priority : int = -2 |
|
127 -- "execution priority of main document structure (e.g. 0, -1, -2)" |
|
128 |
126 |
129 |
127 section "Miscellaneous Tools" |
130 section "Miscellaneous Tools" |
128 |
131 |
129 public option find_theorems_limit : int = 40 |
132 public option find_theorems_limit : int = 40 |
130 -- "limit of displayed results" |
133 -- "limit of displayed results" |