equal
deleted
inserted
replaced
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_reset_font_size : int = 18 |
12 public option jedit_reset_font_size : int = 18 |
13 -- "reset font size for main text area" |
13 -- "reset main text font size" |
14 |
14 |
15 public option jedit_font_scale : real = 1.0 |
15 public option jedit_font_scale : real = 1.0 |
16 -- "scale factor of add-on panels wrt. main text area" |
16 -- "scale factor of add-on panels wrt. main text font" |
17 |
17 |
18 public option jedit_popup_font_scale : real = 0.85 |
18 public option jedit_popup_font_scale : real = 0.85 |
19 -- "scale factor of popups wrt. main text area" |
19 -- "scale factor of popups wrt. main text font" |
20 |
20 |
21 public option jedit_popup_bounds : real = 0.5 |
21 public option jedit_popup_bounds : real = 0.5 |
22 -- "relative bounds of popup window wrt. logical screen size" |
22 -- "relative bounds of popup window wrt. logical screen size" |
23 |
23 |
24 public option jedit_tooltip_delay : real = 0.75 |
24 public option jedit_tooltip_delay : real = 0.75 |