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

[Steffen Juilf Smolka]

The problem is still there on Mountain Lion with an American keyboard.
However, rebinding the kebyoard shortcut locally as you suggested does the trick - thanks for the tip!

Here is an ugly hack (based on the KeyEventDemo you provided) that would solve the problem:

KeyEvent e_ = null;
// pressing a key twice in 5 ms or less is probably impossible
final long eps = 5;

/** Handle the key pressed event from the text field. */
public void keyPressed(final KeyEvent e) {
	final boolean process = e_ == null || e.getKeyCode() != e_.getKeyCode()
			|| (e.getWhen() - e_.getWhen()) > eps;
	e_ = e;
	if (process) {
		displayInfo(e, "KEY PRESSED: ");
	}
}

Steffen 

On 07.01.2013, at 11:07, Makarius <makarius at sketis.net> wrote:

> 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<KeyEventDemo.java>