Pure/Tools/spell_checker.scala

118       (word, upd) <- updates.iterator
120     } yield word
122   private def excluded(word: String): Boolean =
123     updates.get(word) match {
135           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
136         } yield (word, Spell_Checker.Update(include, true))
151       word <- main_dictionary.iterator ++ included_iterator()
152       if !excluded(word)
153     } add.invoke(factory, word)
163         (word, upd) <- updates.iterator
165       } yield Spell_Checker.Decl(word, upd.include)).toList
170 #   * each line contains at most one word
183   def update(word: String, include: Boolean, permanent: Boolean)
185     updates += (word -> Spell_Checker.Update(include, permanent))
189       Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
206   def contains(word: String): Boolean =
208       invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
210   def check(word: String): Boolean =
211     word match {
213         contains(word) || contains(Word.lowercase(word))
215         contains(word)
224   private def suggestions(word: String): Option[List[String]] =
228         invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
232   def complete(word: String): List[String] =
233     if (check(word)) Nil
235       val word_case = Word.Case.unapply(word)
244             suggestions(word) orElse suggestions(Word.lowercase(word))
246             suggestions(word)
255       word <- Spell_Checker.current_word(rendering, caret_range)
256       words = complete(word.info)
260         words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
261     } yield Completion.Result(word.range, word.info, false, items)