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