# HG changeset patch
# User wenzelm
# Date 1397589200 -7200
# Node ID 82be272f79162ca376b250350db7238b2d7bd235
# Parent  e3a06699a13fc23dd3061c93c415998c8acf47b3
more context-sensitivity;

diff -r e3a06699a13f -r 82be272f7916 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 20:24:49 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 21:13:20 2014 +0200
@@ -23,12 +23,6 @@
 {
   /* spell checker menu */
 
-  private def action_item(name: String): JMenuItem =
-  {
-    val context = jEdit.getActionContext()
-    new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
-  }
-
   private def spell_checker_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
   {
     val result =
@@ -38,20 +32,36 @@
         rendering = doc_view.get_rendering()
         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
         Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
-      } yield spell_checker.check(word)
+      } yield (spell_checker, word)
 
     result match {
-      case Some(false) =>
-        List(
-          action_item("isabelle.complete-word"),
-          action_item("isabelle.include-word"),
-          action_item("isabelle.include-word-permanently"),
-          action_item("isabelle.reset-words"))
-      case Some(true) =>
-        List(
-          action_item("isabelle.exclude-word"),
-          action_item("isabelle.exclude-word-permanently"),
-          action_item("isabelle.reset-words"))
+      case Some((spell_checker, word)) =>
+
+        val context = jEdit.getActionContext()
+        def item(name: String): JMenuItem =
+          new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
+
+        val complete_items =
+          if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word"))
+          else Nil
+
+        val update_items =
+          if (spell_checker.check(word))
+            List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
+          else
+            List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
+
+        val reset_items =
+          spell_checker.reset_enabled() match {
+            case 0 => Nil
+            case n =>
+              val name = "isabelle.reset-words"
+              val label = context.getAction(name).getLabel
+              List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
+          }
+
+        complete_items ::: update_items ::: reset_items
+
       case None => Nil
     }
   }
diff -r e3a06699a13f -r 82be272f7916 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 20:24:49 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 21:13:20 2014 +0200
@@ -236,6 +236,9 @@
     load()
   }
 
+  def reset_enabled(): Int =
+    updates.valuesIterator.filter(upd => !upd.permanent).length
+
   def contains(word: String): Boolean =
   {
     val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
@@ -257,6 +260,8 @@
       m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
     }
 
+  def complete_enabled(word: String): Boolean = !complete(word).isEmpty
+
   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
     Spell_Checker.marked_words(base, text, info => !check(info.info))
 }