# HG changeset patch
# User wenzelm
# Date 1275219875 -7200
# Node ID ea52509f4c423ccc9f37a1ecac652c42094025c9
# Parent  2b4e52ecf6fcfdf9fc59aabd25401cd034900ddc
more basic default behaviour of ENTER, HOME, END;

diff -r 2b4e52ecf6fc -r ea52509f4c42 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Sat May 29 20:49:04 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Sun May 30 13:44:35 2010 +0200
@@ -174,11 +174,17 @@
 encoding.opt-out.x-windows-950=true
 encoding.opt-out.x-windows-iso2022jp=true
 encodingDetectors=BOM XML-PI buffer-local-property
+end.shortcut=
 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
 firstTime=false
+home.shortcut=
+insert-newline-indent.shortcut=
+insert-newline.shortcut=ENTER
 isabelle-output.dock-position=bottom
 isabelle-protocol.dock-position=bottom
 isabelle.activate.shortcut=CS+ENTER
+line-end.shortcut=END
+line-home.shortcut=HOME
 mode.isabelle.sidekick.showStatusWindow.label=true
 print.font=IsabelleText
 sidekick-tree.dock-position=right