[isabelle-dev] jedit: zoom with cmd+<+>
Steffen Juilf Smolka
steffen.smolka at in.tum.de
Wed Dec 19 14:21:12 CET 2012
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.
More information about the isabelle-dev