diff -r 0f9d2e13187e -r 2b38472a4695 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Mon Apr 14 20:36:50 2014 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Mon Apr 14 21:51:41 2014 +0200 @@ -211,6 +211,11 @@ isabelle.increase-font-size.shortcut=C+PLUS isabelle.increase-font-size2.label=Increase font size (clone) isabelle.increase-font-size2.shortcut=C+EQUALS +isabelle.include-word.label=Include word +isabelle.include-word-permanently.label=Include word permanently +isabelle.exclude-word.label=Exclude word +isabelle.exclude-word-permanently.label=Exclude word permanently +isabelle.reset-words.label=Reset words isabelle.reset-continuous-checking.label=Reset continuous checking isabelle.reset-font-size.label=Reset font size isabelle.reset-node-required.label=Reset node required