| changeset 55825 | 694833e3e4a0 |
| parent 55618 | 995162143ef4 |
| child 56662 | f373fb77e0a4 |
| 55824:22bc50a19afa | 55825:694833e3e4a0 |
|---|---|
74 |
74 |
75 private def handle_resize() |
75 private def handle_resize() |
76 { |
76 { |
77 Swing_Thread.require() |
77 Swing_Thread.require() |
78 |
78 |
79 pretty_text_area.resize(Rendering.font_family(), |
79 pretty_text_area.resize( |
80 (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round) |
80 Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100)) |
81 } |
81 } |
82 |
82 |
83 |
83 |
84 /* resize */ |
84 /* resize */ |
85 |
85 |