jEdit doesn't recognize the mac option key at all (presumably should map to "meta").
According to conversation on the mailing list, it relates to the following KeyEventTranslator
code:
if(OperatingSystem.isMacOS())
{
setModifierMapping(
InputEvent.META_MASK, /* == C+ */
InputEvent.CTRL_MASK, /* == A+ */
/* M+ discarded by key event workaround! */
InputEvent.ALT_MASK, /* == M+ */
InputEvent.SHIFT_MASK /* == S+ */);
}
else
{
setModifierMapping(
InputEvent.CTRL_MASK,
InputEvent.ALT_MASK,
InputEvent.META_MASK,
InputEvent.SHIFT_MASK);
}
Unfortunately, it looks like the following bug explains why this happens:
https://sourceforge.net/support/tracker.php?aid=816909
The easily solution here is to do things the mac-way and only allow "option" commands
to be used in conjunction with other modifier keys (command or control), similar to
the shift key.
| Submitted | forevermore - 2008-01-15 - 04:49:59z | Assigned | evanpw |
|---|---|---|---|
| Priority | 5 | Category | None |
| Status | Open | Group | None |
| Resolution | None | Visibility | No |
| 2009-12-30 - 09:19:05z ezust |
Personally, I thinik the Mac OSX plugin should offer a nice convenient way of selecting
the different modifier-mappings that are popular, since there are at least 2 settings
that are commonly used, one amongst people who are accustomed to Mac OSX keyboards
and one amongst people who are accustomed to Windows keyboards. But in the meantime, you can change the mappings via some sample code that is found in the settings/startup.bsh file of your default jEdit install. |
|---|