[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 mailing list