refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
--- a/NEWS Mon Apr 07 13:55:12 2014 +0200
+++ b/NEWS Mon Apr 07 16:37:57 2014 +0200
@@ -108,8 +108,7 @@
simplification process, enabled by the newly-introduced
"simplifier_trace" declaration.
-* Support for Navigator plugin, with toolbar buttons and keyboard
-shortcuts similar to major web browsers.
+* Support for Navigator plugin (with toolbar buttons).
*** Pure ***
--- a/src/Tools/jEdit/src/jEdit.props Mon Apr 07 13:55:12 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Mon Apr 07 16:37:57 2014 +0200
@@ -227,8 +227,6 @@
logo.icon.medium=32x32/apps/isabelle.gif
lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
match-bracket.shortcut2=C+9
-navigator.back.shortcut=A+LEFT
-navigator.forward.shortcut=A+RIGHT
navigator.showOnToolbar=true
next-bracket.shortcut2=C+e C+9
plugin-blacklist.MacOSX.jar=true