src/Tools/jEdit/src/jEdit.props
changeset 56574 2b38472a4695
parent 56450 16d4213d4cbc
child 56581 af3e6576e680
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Apr 14 20:36:50 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Apr 14 21:51:41 2014 +0200
     1.3 @@ -211,6 +211,11 @@
     1.4  isabelle.increase-font-size.shortcut=C+PLUS
     1.5  isabelle.increase-font-size2.label=Increase font size (clone)
     1.6  isabelle.increase-font-size2.shortcut=C+EQUALS
     1.7 +isabelle.include-word.label=Include word
     1.8 +isabelle.include-word-permanently.label=Include word permanently
     1.9 +isabelle.exclude-word.label=Exclude word
    1.10 +isabelle.exclude-word-permanently.label=Exclude word permanently
    1.11 +isabelle.reset-words.label=Reset words
    1.12  isabelle.reset-continuous-checking.label=Reset continuous checking
    1.13  isabelle.reset-font-size.label=Reset font size
    1.14  isabelle.reset-node-required.label=Reset node required