src/Pure/Tools/spell_checker.scala
changeset 66117 e6f808d1307c
parent 66116 dad409cd3423
child 66137 d2923067b376
--- a/src/Pure/Tools/spell_checker.scala	Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Mon Jun 19 20:32:06 2017 +0200
@@ -219,7 +219,7 @@
     Spell_Checker.marked_words(base, text, info => !check(info.info))
 
 
-  /* suggestions for unknown words */
+  /* completion: suggestions for unknown words */
 
   private def suggestions(word: String): Option[List[String]] =
   {
@@ -249,6 +249,19 @@
     }
 
   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)
+    for {
+      word <- Spell_Checker.current_word(rendering, caret_range)
+      words = complete(word.info)
+      if words.nonEmpty
+      descr = "(from dictionary " + quote(dictionary.toString) + ")"
+      items =
+        words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
+    } yield Completion.Result(word.range, word.info, false, items)
+  }
 }