equal
deleted
inserted
replaced
4 -- "default logic session" |
4 -- "default logic session" |
5 |
5 |
6 public option jedit_print_mode : string = "" |
6 public option jedit_print_mode : string = "" |
7 -- "default print modes for output, separated by commas (change requires restart)" |
7 -- "default print modes for output, separated by commas (change requires restart)" |
8 |
8 |
9 public option jedit_auto_load : bool = false |
|
10 -- "load all required files automatically to resolve theory imports" |
|
11 |
|
12 public option jedit_auto_resolve : bool = false |
9 public option jedit_auto_resolve : bool = false |
13 -- "automatically resolve auxiliary files within the editor" |
10 -- "automatically resolve auxiliary files within the document model" |
14 |
11 |
15 public option jedit_reset_font_size : int = 18 |
12 public option jedit_reset_font_size : int = 18 |
16 -- "reset main text font size" |
13 -- "reset main text font size" |
17 |
14 |
18 public option jedit_font_scale : real = 1.0 |
15 public option jedit_font_scale : real = 1.0 |