src/Tools/jEdit/src/spell_checker.scala
changeset 56581 af3e6576e680
parent 56577 58d7960058f5
child 56583 c49607db182a
--- 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
       }