tuned menu;
authorwenzelm
Tue Apr 15 00:14:57 2014 +0200 (2014-04-15 ago)
changeset 56581af3e6576e680
parent 56580 f253c4948a97
child 56582 f05b7d6ec592
tuned menu;
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/spell_checker.scala
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 00:07:07 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 00:14:57 2014 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4  isabelle.include-word-permanently.label=Include word permanently
     1.5  isabelle.exclude-word.label=Exclude word
     1.6  isabelle.exclude-word-permanently.label=Exclude word permanently
     1.7 -isabelle.reset-words.label=Reset words
     1.8 +isabelle.reset-words.label=Reset non-permanent words
     1.9  isabelle.reset-continuous-checking.label=Reset continuous checking
    1.10  isabelle.reset-font-size.label=Reset font size
    1.11  isabelle.reset-node-required.label=Reset node required
     2.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 00:07:07 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 00:14:57 2014 +0200
     2.3 @@ -321,9 +321,15 @@
     2.4              new EnhancedMenuItem(context.getAction(action).getLabel, action, context)
     2.5  
     2.6            if (known_word)
     2.7 -            Array(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
     2.8 +            Array(
     2.9 +              item("isabelle.exclude-word"),
    2.10 +              item("isabelle.exclude-word-permanently"),
    2.11 +              item("isabelle.reset-words"))
    2.12            else
    2.13 -            Array(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
    2.14 +            Array(
    2.15 +              item("isabelle.include-word"),
    2.16 +              item("isabelle.include-word-permanently"),
    2.17 +              item("isabelle.reset-words"))
    2.18  
    2.19          case None => null
    2.20        }