equal
deleted
inserted
replaced
12 option jedit_tooltip_font_scale : real = 0.85 |
12 option jedit_tooltip_font_scale : real = 0.85 |
13 -- "scale factor of tooltips wrt. main text area" |
13 -- "scale factor of tooltips wrt. main text area" |
14 |
14 |
15 option jedit_tooltip_margin : int = 60 |
15 option jedit_tooltip_margin : int = 60 |
16 -- "margin for tooltip pretty-printing" |
16 -- "margin for tooltip pretty-printing" |
17 |
|
18 option jedit_tooltip_dismiss_delay : real = 8.0 |
|
19 -- "global delay for Swing tooltips" |
|
20 |
17 |
21 option jedit_text_overview : bool = true |
18 option jedit_text_overview : bool = true |
22 -- "paint text overview column (potentially slow for large files)" |
19 -- "paint text overview column (potentially slow for large files)" |
23 |
20 |
24 |
21 |