equal
deleted
inserted
replaced
225 line-end.shortcut=END |
225 line-end.shortcut=END |
226 line-home.shortcut=HOME |
226 line-home.shortcut=HOME |
227 logo.icon.medium=32x32/apps/isabelle.gif |
227 logo.icon.medium=32x32/apps/isabelle.gif |
228 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel |
228 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel |
229 match-bracket.shortcut2=C+9 |
229 match-bracket.shortcut2=C+9 |
230 navigator.back.shortcut=A+LEFT |
|
231 navigator.forward.shortcut=A+RIGHT |
|
232 navigator.showOnToolbar=true |
230 navigator.showOnToolbar=true |
233 next-bracket.shortcut2=C+e C+9 |
231 next-bracket.shortcut2=C+e C+9 |
234 plugin-blacklist.MacOSX.jar=true |
232 plugin-blacklist.MacOSX.jar=true |
235 plugin.MacOSXPlugin.altDispatcher=false |
233 plugin.MacOSXPlugin.altDispatcher=false |
236 plugin.MacOSXPlugin.disableOption=true |
234 plugin.MacOSXPlugin.disableOption=true |