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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
