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

[Makarius]

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 
key events.


See also the mail thread on "Mac OS X support on Oracle Java 7" that 
Fabian Immler has started recently 
http://sourceforge.net/mailarchive/message.php?msg_id=30165793

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.


 	Makarius