tuned signature;
authorwenzelm
Tue, 20 Jun 2017 11:19:06 +0200
changeset 66137 d2923067b376
parent 66122 ea7c2a245b84
child 66138 f7ef4c50b747
tuned signature;
src/Pure/Tools/spell_checker.scala
src/Tools/jEdit/src/jedit_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)
--- 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 =