# 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)) }