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

[Makarius]

On Sat, 22 Dec 2012, Makarius wrote:

> 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've spent yet more time on the Mac OS X keyboard problem, which resulted
in change 76ae4e6318fb so far -- you will need the jedit_build update from 
the later e7b2cfcef94c to try it yourself.

This now works on all machines I had tried at that point: Windows + Linux 
+ Mac OS X Mountain Lion, all with German keyboard.  Trying it again with 
Mac OS X Snow Leopard and English keyboard, I still see the triplication 
of COMMAND-EQUALS for the Meta "+" key, though.  Testing that with the 
low-level Java key handler that is attached here, it actually shows 3 
KEY_PRESSED events produced by jdk-7u9 on that machine.

So we should blame Oracle or Apple for that ...

If someone comes up with a workaround nonetheless, I will look at it once 
more.


Note that by rebinding the keyboard shortcut yourself locally, it will 
turn the 3 keystrokes happily into just one editor action.


 	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: KeyEventDemo.java
Type: text/x-java
Size: 8197 bytes
Desc: 
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130107/4fba6e21/attachment-0001.java>