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

[Makarius]

On Tue, 8 Jan 2013, Steffen Juilf Smolka wrote:

> 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: ");
> 	}
> }

Before starting such strange patches, we should learn how to submit 
reports to Oracle, maybe by taking http://bugreport.sun.com/bugreport/ as 
a starting point.

I've never done it for JDK myself so far, and I have no idea how long it 
might take for Oracle to move.  When Apple was still in charge of its Java 
own version (until 1.6), I did file reports occasionally, but it was 
hopeleless.  Larry Ellison has promised to do better than Steve Jobs.

I won't do anything here myself before the release, though.  What is more 
immediate for me is to put some (other) patches on some jEdit tracker.


 	Makarius