avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
authorwenzelm
Wed, 09 Oct 2013 23:06:23 +0200
changeset 54318 1bdd8f541a06
parent 54317 da932f511746
child 54319 219dd1028399
avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
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