# 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