Sometimes you need to temporarily change the font size, especially with Japanese text (or any other text too). The standard keys CTRL+ / CTRL- / CTRL mouse wheel would be nice.
Font Size Resizing
jps
#2
Via the API, you can get the font via view.options().get(‘font’) and set it via view.options().set(‘font’, ‘Courier New 12’).
It’d be fairly straightforward to write a plugin that gets the current font, parses it for the font size, and then sets it again with a smaller or larger size. I’ll add it to the todo list unless someone else gets around to it first.
0 Likes