# HG changeset patch
# User wenzelm
# Date 1397513697 -7200
# Node ID af3e6576e680fc83392f08a5dd5cfc14291a50a9
# Parent  f253c4948a97421ccd8bbb348dccd06abfa959e2
tuned menu;

diff -r f253c4948a97 -r af3e6576e680 src/Tools/jEdit/src/jEdit.props
--- 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
diff -r f253c4948a97 -r af3e6576e680 src/Tools/jEdit/src/spell_checker.scala
--- 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
       }