--- a/src/Pure/Tools/spell_checker.scala Mon Jun 19 21:33:29 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala Tue Jun 20 11:19:06 2017 +0200
@@ -248,8 +248,6 @@
result.getOrElse(Nil).map(recover_case)
}
- def complete_enabled(word: String): Boolean = complete(word).nonEmpty
-
def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] =
{
val caret_range = rendering.before_caret_range(caret)
@@ -264,7 +262,6 @@
}
}
-
class Spell_Checker_Variable
{
private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 21:33:29 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Tue Jun 20 11:19:06 2017 +0200
@@ -53,7 +53,7 @@
new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
val complete_items =
- if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word"))
+ if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word"))
else Nil
val update_items =