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 552061bdd8f541a06
parent 55205 da932f511746
child 55207 219dd1028399
avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Wed Oct 09 15:33:20 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Wed Oct 09 23:06:23 2013 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  buffer.sidekick.keystroke-parse=false
     1.5  buffer.tabSize=2
     1.6  close-docking-area.shortcut2=C+e C+CIRCUMFLEX
     1.7 +complete-word.shortcut=
     1.8  console.dock-position=floating
     1.9  console.encoding=UTF-8
    1.10  console.font=IsabelleText
    1.11 @@ -190,8 +191,8 @@
    1.12  isabelle-sledgehammer.dock-position=bottom
    1.13  isabelle-symbols.dock-position=bottom
    1.14  isabelle-theories.dock-position=right
    1.15 -isabelle.complete.label=Complete text
    1.16 -isabelle.complete.shortcut=C+b
    1.17 +isabelle.complete.label=Complete Isabelle text
    1.18 +isabelle.complete.shortcut2=C+b
    1.19  isabelle.control-bold.label=Control bold
    1.20  isabelle.control-bold.shortcut=C+e RIGHT
    1.21  isabelle.control-reset.label=Control reset