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