[isabelle-dev] jedit: zoom with cmd+<+>
makarius at sketis.net
Sat Dec 22 11:13:06 CET 2012
On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote:
> 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).
That was one such convenience that I managed to get working after 20min
Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that
is not finished yet, and there are remaining problems to treat CTRL, ALT,
COMMAND modifiers properly: it can cause duplication or triplication of
See also the mail thread on "Mac OS X support on Oracle Java 7" that
Fabian Immler has started recently
It touches some of the internal issues, including a slightly odd
workaround by myself to modify an older workaround to make it half-working
again under Java 7.
This needs more systematic investigation, by instrumenting the jEdit
sources to produce detailed traces for all critical points where the
MacOSX specific key handling happens. Then it needs to be compared for
Java 6 vs. Java 7, to reconstruct the ideas behind it, which nobody
seems to remember on jedit-devel.
I am unsure if I will manage anything like that myself before the Isabelle
release. Mac OS X poses a bit too many extra problems, and has a bit too
few people actually supporting it actively. On jedit-devel there is right
now exactly one Mac OS X guy hanging around.
More information about the isabelle-dev