equal
deleted
inserted
replaced
55 |
55 |
56 private def handle_resize() |
56 private def handle_resize() |
57 { |
57 { |
58 Swing_Thread.require() |
58 Swing_Thread.require() |
59 |
59 |
60 pretty_text_area.resize(Rendering.font_family(), |
60 pretty_text_area.resize( |
61 (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round) |
61 Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100)) |
62 } |
62 } |
63 |
63 |
64 private val delay_resize = |
64 private val delay_resize = |
65 Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
65 Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
66 |
66 |