Sat, 01 Dec 2012 22:42:54 +0100 wenzelm moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
Sat, 01 Dec 2012 22:23:42 +0100 wenzelm leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip