equal
deleted
inserted
replaced
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 |
9 public option jedit_auto_load : bool = false |
10 -- "load all required files automatically to resolve theory imports" |
10 -- "load all required files automatically to resolve theory imports" |
11 |
11 |
12 public option jedit_auto_resolve : bool = false |
12 public option jedit_auto_resolve : bool = true |
13 -- "automatically resolve auxiliary files within the editor" |
13 -- "automatically resolve auxiliary files within the editor" |
14 |
14 |
15 public option jedit_reset_font_size : int = 18 |
15 public option jedit_reset_font_size : int = 18 |
16 -- "reset main text font size" |
16 -- "reset main text font size" |
17 |
17 |