# HG changeset patch # User wenzelm # Date 1381352783 -7200 # Node ID 1bdd8f541a066ee7b8529fab511285011f727a8e # Parent da932f511746aefe31e786184a1e59bf27100450 avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus); diff -r da932f511746 -r 1bdd8f541a06 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Wed Oct 09 15:33:20 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Wed Oct 09 23:06:23 2013 +0200 @@ -9,6 +9,7 @@ buffer.sidekick.keystroke-parse=false buffer.tabSize=2 close-docking-area.shortcut2=C+e C+CIRCUMFLEX +complete-word.shortcut= console.dock-position=floating console.encoding=UTF-8 console.font=IsabelleText @@ -190,8 +191,8 @@ isabelle-sledgehammer.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right -isabelle.complete.label=Complete text -isabelle.complete.shortcut=C+b +isabelle.complete.label=Complete Isabelle text +isabelle.complete.shortcut2=C+b isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-reset.label=Control reset