# HG changeset patch
# User wenzelm
# Date 1497950346 -7200
# Node ID d2923067b3760083b22fa74c0183ba2a0a3337dc
# Parent  ea7c2a245b84803aebfa3e09c69d5a2bde140451
tuned signature;

diff -r ea7c2a245b84 -r d2923067b376 src/Pure/Tools/spell_checker.scala
--- 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)
diff -r ea7c2a245b84 -r d2923067b376 src/Tools/jEdit/src/jedit_spell_checker.scala
--- 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 =