equal
deleted
inserted
replaced
125 |
125 |
126 option editor_execution_priority : int = -1 |
126 option editor_execution_priority : int = -1 |
127 -- "execution priority of main document structure (e.g. 0, -1, -2)" |
127 -- "execution priority of main document structure (e.g. 0, -1, -2)" |
128 |
128 |
129 option editor_execution_range : string = "visible" |
129 option editor_execution_range : string = "visible" |
130 -- "range of continuous document processing: all, none, visible" |
130 -- "execution range of continuous document processing: all, none, visible" |
131 |
131 |
132 |
132 |
133 section "Miscellaneous Tools" |
133 section "Miscellaneous Tools" |
134 |
134 |
135 public option find_theorems_limit : int = 40 |
135 public option find_theorems_limit : int = 40 |