--- a/src/Tools/jEdit/src/jEdit.props Tue Apr 15 00:07:07 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue Apr 15 00:14:57 2014 +0200
@@ -215,7 +215,7 @@
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-words.label=Reset non-permanent 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
--- a/src/Tools/jEdit/src/spell_checker.scala Tue Apr 15 00:07:07 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Tue Apr 15 00:14:57 2014 +0200
@@ -321,9 +321,15 @@
new EnhancedMenuItem(context.getAction(action).getLabel, action, context)
if (known_word)
- Array(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
+ Array(
+ item("isabelle.exclude-word"),
+ item("isabelle.exclude-word-permanently"),
+ item("isabelle.reset-words"))
else
- Array(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
+ Array(
+ item("isabelle.include-word"),
+ item("isabelle.include-word-permanently"),
+ item("isabelle.reset-words"))
case None => null
}