[isabelle-dev] jedit: zoom with cmd+<+>

[Steffen Juilf Smolka]

Hi,

in a39250169636, it is possible to increase/decrease the font size in jedit with cmd+<+>/cmd+<-> on MacOS (probably ctrl+<+>/ctrl+<-> on other plattforms) (nice feature!). However, pressing  cmd+<+> increases the font size twice on my machine (cmd+<-> works fine).

On a related note, it would be nice to have the shortcut cmd+0 (ctrl+0) for switching to the default font size as well, as it is common in web browsers.

Regards,
Steffen